Theorem mpanl2 698

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpanr1  700  mp3an2  1448  reuss  4250  tfrlem11  8219  tfr3  8230  oe0  8352  unfi  8955  dif1enALT  9050  indpi  10663  map2psrpr  10866  axcnre  10920  muleqadd  11619  divdiv2  11687  addltmul  12209  supxrpnf  13052  supxrunb1  13053  supxrunb2  13054  iimulcl  24100  clwwlknonex2lem2  28472  nmopadjlem  30451  nmopcoadji  30463  opsqrlem6  30507  hstrbi  30628  sgncl  32505  poimirlem3  35780  aacllem  46505