Theorem mpanl2 697

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpanr1  699  mp3an2  1441  reuss  4204  tfrlem11  7876  tfr3  7887  oe0  7998  dif1en  8597  indpi  10175  map2psrpr  10378  axcnre  10432  muleqadd  11132  divdiv2  11200  addltmul  11721  frnnn0supp  11801  supxrpnf  12561  supxrunb1  12562  supxrunb2  12563  iimulcl  23224  clwwlknonex2lem2  27574  nmopadjlem  29557  nmopcoadji  29569  opsqrlem6  29613  hstrbi  29734  sgncl  31413  poimirlem3  34426  aacllem  44382