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  4290  tfrlem11  8356  tfr3  8367  oe0  8486  unfi  9135  dif1ennnALT  9222  indpi  10860  map2psrpr  11063  axcnre  11117  muleqadd  11822  divdiv2  11894  addltmul  12418  supxrpnf  13278  supxrunb1  13279  supxrunb2  13280  iimulcl  24833  clwwlknonex2lem2  30037  nmopadjlem  32018  nmopcoadji  32030  opsqrlem6  32074  hstrbi  32195  sgncl  32756  poimirlem3  37617  dflim5  43318  aacllem  49790