Theorem mpanl2 714

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpanl2.1	⊢ 𝜓
mpanl2.2	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpanl2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpanl2

Step	Hyp	Ref	Expression
1		mpanl2.1	. . 3 ⊢ 𝜓
2	1	jctr 534	. 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓))
3		mpanl2.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 592	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:  mpanr1  716  mp3an2  1478  reuss  4273  tfrlem11  8380  tfr3  8391  oe0  8514  unfi  9170  dif1ennnALT  9252  indpi  10973  map2psrpr  11176  axcnre  11230  muleqadd  11941  divdiv2  12010  addltmul  12563  supxrpnf  13429  supxrunb1  13430  supxrunb2  13431  sgncl  15230  iimulcl  25238  clwwlknonex2lem2  30681  nmopadjlem  32673  nmopcoadji  32685  opsqrlem6  32729  hstrbi  32850  poimirlem3  38509  dflim5  44289  aacllem  50883