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  4277  tfrlem11  8307  tfr3  8318  oe0  8437  unfi  9080  dif1ennnALT  9161  indpi  10795  map2psrpr  10998  axcnre  11052  muleqadd  11758  divdiv2  11830  addltmul  12354  supxrpnf  13214  supxrunb1  13215  supxrunb2  13216  iimulcl  24858  clwwlknonex2lem2  30083  nmopadjlem  32064  nmopcoadji  32076  opsqrlem6  32120  hstrbi  32241  sgncl  32809  poimirlem3  37662  dflim5  43361  aacllem  49832