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  6978  op1steq  7971  fpmg  8798  pmresg  8800  pw2f1o  9002  pm54.43  9901  dfac2b  10029  ttukeylem6  10412  gruina  10716  muleqadd  11768  divdiv1  11839  addltmul  12364  elfzp1b  13503  elfzm1b  13504  expp1z  14020  expm1  14021  oddvdsnn0  19458  efgi0  19634  efgi1  19635  gsumle  20059  fiinbas  22868  opnneissb  23030  fclscf  23941  blssec  24351  iimulcl  24861  itg2lr  25659  blocnilem  30786  lnopmul  31949  opsqrlem6  32127  gsumvsca1  33202  gsumvsca2  33203  locfinreflem  33874  fvray  36206  fvline  36209  fneref  36415  poimirlem3  37684  poimirlem16  37697  fdc  37806  linepmap  39895  rmyeq0  43071  omssaxinf2  45106