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  4276  tfrlem11  8313  tfr3  8324  oe0  8443  unfi  9087  dif1ennnALT  9168  indpi  10805  map2psrpr  11008  axcnre  11062  muleqadd  11768  divdiv2  11840  addltmul  12364  supxrpnf  13219  supxrunb1  13220  supxrunb2  13221  iimulcl  24861  clwwlknonex2lem2  30090  nmopadjlem  32071  nmopcoadji  32083  opsqrlem6  32127  hstrbi  32248  sgncl  32819  poimirlem3  37683  dflim5  43446  aacllem  49926