Theorem mpanr2 717

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fvreseq1  7030  op1steq  8034  fpmg  8880  pmresg  8882  pw2f1o  9085  pm54.43  10063  dfac2b  10190  ttukeylem6  10573  gruina  10884  muleqadd  11941  divdiv1  12009  addltmul  12563  elfzp1b  13715  elfzm1b  13716  expp1z  14234  expm1  14235  oddvdsnn0  19738  efgi0  19914  efgi1  19915  gsumle  20339  fiinbas  23250  opnneissb  23412  fclscf  24324  blssec  24734  iimulcl  25238  itg2lr  26031  blocnilem  31388  lnopmul  32551  opsqrlem6  32729  gsumvsca1  33769  gsumvsca2  33770  locfinreflem  34454  fvray  36876  fvline  36879  fneref  37108  poimirlem3  38509  poimirlem16  38522  fdc  38647  linepmap  40800  rmyeq0  43913  omssaxinf2  45930