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  4267  tfrlem11  8327  tfr3  8338  oe0  8457  unfi  9105  dif1ennnALT  9187  indpi  10830  map2psrpr  11033  axcnre  11087  muleqadd  11794  divdiv2  11867  addltmul  12413  supxrpnf  13270  supxrunb1  13271  supxrunb2  13272  iimulcl  24904  clwwlknonex2lem2  30178  nmopadjlem  32160  nmopcoadji  32172  opsqrlem6  32216  hstrbi  32337  sgncl  32904  poimirlem3  37944  dflim5  43757  aacllem  50276