Theorem mpanl2 716

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  mpanr1  718  mp3an2  1409  reuss  3890  tfrlem11  7444  tfr3  7455  oe0  7562  dif1en  8153  indpi  9689  map2psrpr  9891  axcnre  9945  muleqadd  10631  divdiv2  10697  addltmul  11228  frnnn0supp  11309  supxrpnf  12107  supxrunb1  12108  supxrunb2  12109  iimulcl  22676  numclwwlkovf2ex  27109  eigposi  28583  nmopadjlem  28836  nmopcoadji  28848  opsqrlem6  28892  hstrbi  29013  sgncl  30423  poimirlem3  33083  aacllem  41880