Theorem mpanl2 701

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 524	. 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓))
3		mpanl2.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	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:  mpanr1  703  mp3an2  1451  reuss  4276  tfrlem11  8313  tfr3  8324  oe0  8443  unfi  9086  dif1ennnALT  9167  indpi  10804  map2psrpr  11007  axcnre  11061  muleqadd  11767  divdiv2  11839  addltmul  12363  supxrpnf  13223  supxrunb1  13224  supxrunb2  13225  iimulcl  24866  clwwlknonex2lem2  30095  nmopadjlem  32076  nmopcoadji  32088  opsqrlem6  32132  hstrbi  32253  sgncl  32821  poimirlem3  37669  dflim5  43427  aacllem  49907