Theorem mpanl2 702

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 581	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  704  mp3an2  1452  reuss  4281  tfrlem11  8329  tfr3  8340  oe0  8459  unfi  9107  dif1ennnALT  9189  indpi  10830  map2psrpr  11033  axcnre  11087  muleqadd  11793  divdiv2  11865  addltmul  12389  supxrpnf  13245  supxrunb1  13246  supxrunb2  13247  iimulcl  24901  clwwlknonex2lem2  30195  nmopadjlem  32176  nmopcoadji  32188  opsqrlem6  32232  hstrbi  32353  sgncl  32922  poimirlem3  37868  dflim5  43680  aacllem  50154