Theorem mpanr2 701

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 525	. 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒))
3		mpanr2.2	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	sylan2 593	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 206  df-an 397

This theorem is referenced by:  fvreseq1  6916  op1steq  7875  fpmg  8656  pmresg  8658  pw2f1o  8864  pm54.43  9759  dfac2b  9886  ttukeylem6  10270  gruina  10574  muleqadd  11619  divdiv1  11686  addltmul  12209  elfzp1b  13333  elfzm1b  13334  expp1z  13832  expm1  13833  oddvdsnn0  19152  efgi0  19326  efgi1  19327  fiinbas  22102  opnneissb  22265  fclscf  23176  blssec  23588  iimulcl  24100  itg2lr  24895  blocnilem  29166  lnopmul  30329  opsqrlem6  30507  gsumle  31350  gsumvsca1  31479  gsumvsca2  31480  locfinreflem  31790  fvray  34443  fvline  34446  fneref  34539  poimirlem3  35780  poimirlem16  35793  fdc  35903  linepmap  37789  rmyeq0  40775