Theorem mpanl2 701

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 580	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  703  mp3an2  1451  reuss  4279  tfrlem11  8319  tfr3  8330  oe0  8449  unfi  9095  dif1ennnALT  9177  indpi  10818  map2psrpr  11021  axcnre  11075  muleqadd  11781  divdiv2  11853  addltmul  12377  supxrpnf  13233  supxrunb1  13234  supxrunb2  13235  iimulcl  24889  clwwlknonex2lem2  30183  nmopadjlem  32164  nmopcoadji  32176  opsqrlem6  32220  hstrbi  32341  sgncl  32912  poimirlem3  37820  dflim5  43567  aacllem  50042