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 528	. 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓))
3		mpanl2.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 583	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 210  df-an 400

This theorem is referenced by:  mpanr1  703  mp3an2  1451  reuss  4231  tfrlem11  8124  tfr3  8135  oe0  8249  unfi  8850  dif1enALT  8907  indpi  10521  map2psrpr  10724  axcnre  10778  muleqadd  11476  divdiv2  11544  addltmul  12066  supxrpnf  12908  supxrunb1  12909  supxrunb2  12910  iimulcl  23834  clwwlknonex2lem2  28191  nmopadjlem  30170  nmopcoadji  30182  opsqrlem6  30226  hstrbi  30347  sgncl  32217  poimirlem3  35517  aacllem  46176