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  8380  tfr3  8391  oe0  8512  unfi  9168  dif1ennnALT  9250  indpi  10919  map2psrpr  11122  axcnre  11176  muleqadd  11885  divdiv2  11954  addltmul  12507  supxrpnf  13372  supxrunb1  13373  supxrunb2  13374  sgncl  15172  iimulcl  25166  clwwlknonex2lem2  30564  nmopadjlem  32556  nmopcoadji  32568  opsqrlem6  32612  hstrbi  32733  poimirlem3  38359  dflim5  44157  aacllem  50759