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  6482  op1steq  7378  fpmg  8051  pmresg  8053  pw2f1o  8232  pm54.43  9036  dfac2b  9163  dfac2OLD  9165  ttukeylem6  9548  gruina  9852  muleqadd  10883  divdiv1  10948  addltmul  11480  elfzp1b  12630  elfzm1b  12631  expp1z  13123  expm1  13124  oddvdsnn0  18183  efgi0  18353  efgi1  18354  fiinbas  20978  opnneissb  21140  fclscf  22050  blssec  22461  iimulcl  22957  itg2lr  23716  blocnilem  27989  lnopmul  29156  opsqrlem6  29334  gsumle  30109  gsumvsca1  30112  gsumvsca2  30113  locfinreflem  30237  fvray  32575  fvline  32578  fneref  32672  poimirlem3  33743  poimirlem16  33756  fdc  33872  linepmap  35582  rmyeq0  38040