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 524	. 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓))
3		mpanl2.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 579	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  702  mp3an2  1449  reuss  4346  tfrlem11  8444  tfr3  8455  oe0  8578  unfi  9238  dif1ennnALT  9339  indpi  10976  map2psrpr  11179  axcnre  11233  muleqadd  11934  divdiv2  12006  addltmul  12529  supxrpnf  13380  supxrunb1  13381  supxrunb2  13382  iimulcl  24985  clwwlknonex2lem2  30140  nmopadjlem  32121  nmopcoadji  32133  opsqrlem6  32177  hstrbi  32298  sgncl  34503  poimirlem3  37583  dflim5  43291  aacllem  48895