Theorem mpanr2 720

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpanr2.1	⊢ 𝜒
mpanr2.2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr2	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mpanr2

Step	Hyp	Ref	Expression
1		mpanr2.1	. . 3 ⊢ 𝜒
2	1	jctr 565	. 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒))
3		mpanr2.2	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	sylan2 491	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  fvreseq1  6318  op1steq  7210  fpmg  7883  pmresg  7885  pw2f1o  8065  pm54.43  8826  dfac2  8953  ttukeylem6  9336  gruina  9640  muleqadd  10671  divdiv1  10736  addltmul  11268  elfzp1b  12417  elfzm1b  12418  expp1z  12909  expm1  12910  oddvdsnn0  17963  efgi0  18133  efgi1  18134  fiinbas  20756  opnneissb  20918  fclscf  21829  blssec  22240  iimulcl  22736  itg2lr  23497  blocnilem  27659  lnopmul  28826  opsqrlem6  29004  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  locfinreflem  29907  fvray  32248  fvline  32251  fneref  32345  poimirlem3  33412  poimirlem16  33425  fdc  33541  linepmap  35061  rmyeq0  37520