Theorem mpanr2 704

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fvreseq1  6973  op1steq  7968  fpmg  8795  pmresg  8797  pw2f1o  8999  pm54.43  9897  dfac2b  10025  ttukeylem6  10408  gruina  10712  muleqadd  11764  divdiv1  11835  addltmul  12360  elfzp1b  13504  elfzm1b  13505  expp1z  14018  expm1  14019  oddvdsnn0  19423  efgi0  19599  efgi1  19600  gsumle  20024  fiinbas  22837  opnneissb  22999  fclscf  23910  blssec  24321  iimulcl  24831  itg2lr  25629  blocnilem  30748  lnopmul  31911  opsqrlem6  32089  gsumvsca1  33168  gsumvsca2  33169  locfinreflem  33807  fvray  36115  fvline  36118  fneref  36324  poimirlem3  37603  poimirlem16  37616  fdc  37725  linepmap  39754  rmyeq0  42926  omssaxinf2  44962