Theorem mpanl2 711

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  mpanr1  713  mp3an2  1469  reuss  4279  tfrlem11  8354  tfr3  8365  oe0  8486  unfi  9135  dif1ennnALT  9217  indpi  10862  map2psrpr  11065  axcnre  11119  muleqadd  11828  divdiv2  11900  addltmul  12454  supxrpnf  13318  supxrunb1  13319  supxrunb2  13320  iimulcl  24979  clwwlknonex2lem2  30256  nmopadjlem  32238  nmopcoadji  32250  opsqrlem6  32294  hstrbi  32415  sgncl  32983  poimirlem3  38086  dflim5  43870  aacllem  50386