Theorem mpanl2 702

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanr1  704  mp3an2  1452  reuss  4268  tfrlem11  8320  tfr3  8331  oe0  8450  unfi  9098  dif1ennnALT  9180  indpi  10821  map2psrpr  11024  axcnre  11078  muleqadd  11785  divdiv2  11858  addltmul  12404  supxrpnf  13261  supxrunb1  13262  supxrunb2  13263  iimulcl  24914  clwwlknonex2lem2  30193  nmopadjlem  32175  nmopcoadji  32187  opsqrlem6  32231  hstrbi  32352  sgncl  32919  poimirlem3  37958  dflim5  43775  aacllem  50288