Theorem mpanr2 704

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fvreseq1  6972  op1steq  7965  fpmg  8792  pmresg  8794  pw2f1o  8995  pm54.43  9894  dfac2b  10022  ttukeylem6  10405  gruina  10709  muleqadd  11761  divdiv1  11832  addltmul  12357  elfzp1b  13501  elfzm1b  13502  expp1z  14018  expm1  14019  oddvdsnn0  19457  efgi0  19633  efgi1  19634  gsumle  20058  fiinbas  22868  opnneissb  23030  fclscf  23941  blssec  24351  iimulcl  24861  itg2lr  25659  blocnilem  30782  lnopmul  31945  opsqrlem6  32123  gsumvsca1  33193  gsumvsca2  33194  locfinreflem  33851  fvray  36181  fvline  36184  fneref  36390  poimirlem3  37669  poimirlem16  37682  fdc  37791  linepmap  39820  rmyeq0  42992  omssaxinf2  45027