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  1450  reuss  4326  tfrlem11  8429  tfr3  8440  oe0  8561  unfi  9212  dif1ennnALT  9312  indpi  10948  map2psrpr  11151  axcnre  11205  muleqadd  11908  divdiv2  11980  addltmul  12504  supxrpnf  13361  supxrunb1  13362  supxrunb2  13363  iimulcl  24967  clwwlknonex2lem2  30128  nmopadjlem  32109  nmopcoadji  32121  opsqrlem6  32165  hstrbi  32286  sgncl  34542  poimirlem3  37631  dflim5  43347  aacllem  49375