Theorem mpanr2 722

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  fvreseq1  6469  op1steq  7365  fpmg  8037  pmresg  8039  pw2f1o  8218  pm54.43  8987  dfac2b  9114  dfac2OLD  9116  ttukeylem6  9499  gruina  9803  muleqadd  10834  divdiv1  10899  addltmul  11431  elfzp1b  12581  elfzm1b  12582  expp1z  13074  expm1  13075  oddvdsnn0  18134  efgi0  18304  efgi1  18305  fiinbas  20929  opnneissb  21091  fclscf  22001  blssec  22412  iimulcl  22908  itg2lr  23667  blocnilem  27939  lnopmul  29106  opsqrlem6  29284  gsumle  30059  gsumvsca1  30062  gsumvsca2  30063  locfinreflem  30187  fvray  32525  fvline  32528  fneref  32622  poimirlem3  33694  poimirlem16  33707  fdc  33823  linepmap  35533  rmyeq0  37991