Theorem mpanl2 699

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 527	. 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓))
3		mpanl2.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 582	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanr1  701  mp3an2  1445  reuss  4284  tfrlem11  8018  tfr3  8029  oe0  8141  dif1en  8745  indpi  10323  map2psrpr  10526  axcnre  10580  muleqadd  11278  divdiv2  11346  addltmul  11867  frnnn0supp  11947  supxrpnf  12705  supxrunb1  12706  supxrunb2  12707  iimulcl  23535  clwwlknonex2lem2  27881  nmopadjlem  29860  nmopcoadji  29872  opsqrlem6  29916  hstrbi  30037  sgncl  31791  poimirlem3  34889  aacllem  44895