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  7035  op1steq  8034  fpmg  8879  pmresg  8881  pw2f1o  9084  pm54.43  10010  dfac2b  10137  ttukeylem6  10520  gruina  10831  muleqadd  11886  divdiv1  11954  addltmul  12508  elfzp1b  13660  elfzm1b  13661  expp1z  14179  expm1  14180  oddvdsnn0  19677  efgi0  19853  efgi1  19854  gsumle  20278  fiinbas  23183  opnneissb  23345  fclscf  24257  blssec  24667  iimulcl  25171  itg2lr  25964  blocnilem  31293  lnopmul  32456  opsqrlem6  32634  gsumvsca1  33674  gsumvsca2  33675  locfinreflem  34358  fvray  36729  fvline  36732  fneref  36977  poimirlem3  38380  poimirlem16  38393  fdc  38503  linepmap  40656  rmyeq0  43802  omssaxinf2  45819