Theorem mpanr2 716

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fvreseq1  7024  op1steq  8018  fpmg  8854  pmresg  8856  pw2f1o  9058  pm54.43  9975  dfac2b  10102  ttukeylem6  10486  gruina  10791  muleqadd  11846  divdiv1  11914  addltmul  12468  elfzp1b  13617  elfzm1b  13618  expp1z  14135  expm1  14136  oddvdsnn0  19602  efgi0  19778  efgi1  19779  gsumle  20203  fiinbas  23066  opnneissb  23228  fclscf  24139  blssec  24549  iimulcl  25053  itg2lr  25846  blocnilem  31061  lnopmul  32224  opsqrlem6  32402  gsumvsca1  33454  gsumvsca2  33455  locfinreflem  34142  fvray  36499  fvline  36502  fneref  36718  poimirlem3  38129  poimirlem16  38142  fdc  38251  linepmap  40406  rmyeq0  43537  omssaxinf2  45556