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  1473  reuss  4282  tfrlem11  8363  tfr3  8374  oe0  8495  unfi  9143  dif1ennnALT  9225  indpi  10880  map2psrpr  11083  axcnre  11137  muleqadd  11846  divdiv2  11918  addltmul  12471  supxrpnf  13335  supxrunb1  13336  supxrunb2  13337  sgncl  15124  iimulcl  25057  clwwlknonex2lem2  30368  nmopadjlem  32350  nmopcoadji  32362  opsqrlem6  32406  hstrbi  32527  poimirlem3  38134  dflim5  43918  aacllem  50430