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  1448  reuss  4333  tfrlem11  8427  tfr3  8438  oe0  8559  unfi  9210  dif1ennnALT  9309  indpi  10945  map2psrpr  11148  axcnre  11202  muleqadd  11905  divdiv2  11977  addltmul  12500  supxrpnf  13357  supxrunb1  13358  supxrunb2  13359  iimulcl  24980  clwwlknonex2lem2  30137  nmopadjlem  32118  nmopcoadji  32130  opsqrlem6  32174  hstrbi  32295  sgncl  34520  poimirlem3  37610  dflim5  43319  aacllem  49032