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  4293  tfrlem11  8359  tfr3  8370  oe0  8489  unfi  9141  dif1ennnALT  9229  indpi  10867  map2psrpr  11070  axcnre  11124  muleqadd  11829  divdiv2  11901  addltmul  12425  supxrpnf  13285  supxrunb1  13286  supxrunb2  13287  iimulcl  24840  clwwlknonex2lem2  30044  nmopadjlem  32025  nmopcoadji  32037  opsqrlem6  32081  hstrbi  32202  sgncl  32763  poimirlem3  37624  dflim5  43325  aacllem  49794