Theorem mpanl2 700

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mpanr1  702  mp3an2  1450  reuss  4317  tfrlem11  8388  tfr3  8399  oe0  8522  unfi  9172  dif1ennnALT  9277  indpi  10902  map2psrpr  11105  axcnre  11159  muleqadd  11858  divdiv2  11926  addltmul  12448  supxrpnf  13297  supxrunb1  13298  supxrunb2  13299  iimulcl  24453  clwwlknonex2lem2  29361  nmopadjlem  31342  nmopcoadji  31354  opsqrlem6  31398  hstrbi  31519  sgncl  33537  poimirlem3  36491  dflim5  42079  aacllem  47848