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  4307  tfrlem11  8407  tfr3  8418  oe0  8539  unfi  9190  dif1ennnALT  9288  indpi  10926  map2psrpr  11129  axcnre  11183  muleqadd  11886  divdiv2  11958  addltmul  12482  supxrpnf  13339  supxrunb1  13340  supxrunb2  13341  iimulcl  24889  clwwlknonex2lem2  30094  nmopadjlem  32075  nmopcoadji  32087  opsqrlem6  32131  hstrbi  32252  sgncl  32815  poimirlem3  37652  dflim5  43320  aacllem  49632