Theorem mpanl2 707

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpanr1  709  mp3an2  1457  reuss  4262  tfrlem11  8324  tfr3  8335  oe0  8454  unfi  9102  dif1ennnALT  9184  indpi  10828  map2psrpr  11031  axcnre  11085  muleqadd  11792  divdiv2  11865  addltmul  12411  supxrpnf  13268  supxrunb1  13269  supxrunb2  13270  iimulcl  24929  clwwlknonex2lem2  30203  nmopadjlem  32185  nmopcoadji  32197  opsqrlem6  32241  hstrbi  32362  sgncl  32930  poimirlem3  37997  dflim5  43781  aacllem  50298