Theorem mpanr2 714

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 532	. 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒))
3		mpanr2.2	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	sylan2 602	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fvreseq1  7014  op1steq  8008  fpmg  8843  pmresg  8845  pw2f1o  9047  pm54.43  9952  dfac2b  10080  ttukeylem6  10464  gruina  10769  muleqadd  11824  divdiv1  11895  addltmul  12450  elfzp1b  13599  elfzm1b  13600  expp1z  14117  expm1  14118  oddvdsnn0  19574  efgi0  19750  efgi1  19751  gsumle  20175  fiinbas  22999  opnneissb  23161  fclscf  24072  blssec  24482  iimulcl  24986  itg2lr  25779  blocnilem  30963  lnopmul  32126  opsqrlem6  32304  gsumvsca1  33366  gsumvsca2  33367  locfinreflem  34097  fvray  36451  fvline  36454  fneref  36670  poimirlem3  38082  poimirlem16  38095  fdc  38204  linepmap  40359  rmyeq0  43490  omssaxinf2  45524