Theorem mpanl2 699

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanr1  701  mp3an2  1445  reuss  4287  tfrlem11  8027  tfr3  8038  oe0  8150  dif1en  8754  indpi  10332  map2psrpr  10535  axcnre  10589  muleqadd  11287  divdiv2  11355  addltmul  11876  frnnn0supp  11956  supxrpnf  12714  supxrunb1  12715  supxrunb2  12716  iimulcl  23544  clwwlknonex2lem2  27890  nmopadjlem  29869  nmopcoadji  29881  opsqrlem6  29925  hstrbi  30046  sgncl  31800  poimirlem3  34899  aacllem  44909