Theorem mpanl2 681

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  mpanr1  683  mp3an2  1560  reuss  4056  tfrlem11  7637  tfr3  7648  oe0  7756  dif1en  8349  indpi  9931  map2psrpr  10133  axcnre  10187  muleqadd  10873  divdiv2  10939  addltmul  11470  frnnn0supp  11551  supxrpnf  12353  supxrunb1  12354  supxrunb2  12355  iimulcl  22956  clwwlknonex2lem2  27284  nmopadjlem  29288  nmopcoadji  29300  opsqrlem6  29344  hstrbi  29465  sgncl  30940  poimirlem3  33745  aacllem  43078