Theorem mpanl2 714

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanr1  716  mp3an2  1478  reuss  4276  tfrlem11  8381  tfr3  8392  oe0  8513  unfi  9169  dif1ennnALT  9251  indpi  10920  map2psrpr  11123  axcnre  11177  muleqadd  11886  divdiv2  11955  addltmul  12508  supxrpnf  13374  supxrunb1  13375  supxrunb2  13376  sgncl  15174  iimulcl  25171  clwwlknonex2lem2  30586  nmopadjlem  32578  nmopcoadji  32590  opsqrlem6  32634  hstrbi  32755  poimirlem3  38380  dflim5  44178  aacllem  50780