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  1479  reuss  4275  tfrlem11  8427  tfr3  8438  oe0  8561  unfi  9217  dif1ennnALT  9299  indpi  11022  map2psrpr  11225  axcnre  11279  muleqadd  11990  divdiv2  12059  addltmul  12612  supxrpnf  13478  supxrunb1  13479  supxrunb2  13480  sgncl  15282  iimulcl  25291  clwwlknonex2lem2  30732  nmopadjlem  32724  nmopcoadji  32736  opsqrlem6  32780  hstrbi  32901  poimirlem3  38746  dflim5  44534  aacllem  51251