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  7034  op1steq  8037  fpmg  8887  pmresg  8889  pw2f1o  9096  pm54.43  10020  dfac2b  10150  ttukeylem6  10533  gruina  10837  muleqadd  11886  divdiv1  11957  addltmul  12482  elfzp1b  13623  elfzm1b  13624  expp1z  14134  expm1  14135  oddvdsnn0  19530  efgi0  19706  efgi1  19707  fiinbas  22895  opnneissb  23057  fclscf  23968  blssec  24379  iimulcl  24889  itg2lr  25688  blocnilem  30790  lnopmul  31953  opsqrlem6  32131  gsumle  33097  gsumvsca1  33228  gsumvsca2  33229  locfinreflem  33876  fvray  36164  fvline  36167  fneref  36373  poimirlem3  37652  poimirlem16  37665  fdc  37774  linepmap  39799  rmyeq0  42944  omssaxinf2  44980