Theorem mpanl2 713

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanr1  715  mp3an2  1478  reuss  4281  tfrlem11  8376  tfr3  8387  oe0  8508  unfi  9156  dif1ennnALT  9238  indpi  10893  map2psrpr  11096  axcnre  11150  muleqadd  11859  divdiv2  11928  addltmul  12481  supxrpnf  13345  supxrunb1  13346  supxrunb2  13347  sgncl  15136  iimulcl  25077  clwwlknonex2lem2  30440  nmopadjlem  32422  nmopcoadji  32434  opsqrlem6  32478  hstrbi  32599  poimirlem3  38255  dflim5  44039  aacllem  50584