Theorem mpanr2 710

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fvreseq1  6987  op1steq  7982  fpmg  8813  pmresg  8815  pw2f1o  9017  pm54.43  9923  dfac2b  10051  ttukeylem6  10434  gruina  10739  muleqadd  11792  divdiv1  11864  addltmul  12411  elfzp1b  13553  elfzm1b  13554  expp1z  14071  expm1  14072  oddvdsnn0  19517  efgi0  19693  efgi1  19694  gsumle  20118  fiinbas  22942  opnneissb  23104  fclscf  24015  blssec  24425  iimulcl  24929  itg2lr  25722  blocnilem  30900  lnopmul  32063  opsqrlem6  32241  gsumvsca1  33314  gsumvsca2  33315  locfinreflem  34031  fvray  36376  fvline  36379  fneref  36585  poimirlem3  37997  poimirlem16  38010  fdc  38119  linepmap  40274  rmyeq0  43405  omssaxinf2  45439