Theorem mpanr2 702

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  fvreseq1  7047  op1steq  8038  fpmg  8887  pmresg  8889  pw2f1o  9102  pm54.43  10026  dfac2b  10155  ttukeylem6  10539  gruina  10843  muleqadd  11890  divdiv1  11958  addltmul  12481  elfzp1b  13613  elfzm1b  13614  expp1z  14112  expm1  14113  oddvdsnn0  19511  efgi0  19687  efgi1  19688  fiinbas  22899  opnneissb  23062  fclscf  23973  blssec  24385  iimulcl  24904  itg2lr  25704  blocnilem  30686  lnopmul  31849  opsqrlem6  32027  gsumle  32894  gsumvsca1  33025  gsumvsca2  33026  locfinreflem  33572  fvray  35868  fvline  35871  fneref  35965  poimirlem3  37227  poimirlem16  37240  fdc  37349  linepmap  39378  rmyeq0  42516