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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpanr1  715  mp3an2  1404  reuss  3867  tfrlem11  7371  tfr3  7382  oe0  7489  dif1en  8078  indpi  9608  map2psrpr  9810  axcnre  9864  muleqadd  10550  divdiv2  10616  addltmul  11145  frnnn0supp  11226  supxrpnf  12020  supxrunb1  12021  supxrunb2  12022  iimulcl  22544  numclwwlkovf2ex  26613  eigposi  28079  nmopadjlem  28332  nmopcoadji  28344  opsqrlem6  28388  hstrbi  28509  sgncl  29927  poimirlem3  32582  av-numclwwlkovf2ex  41517  aacllem  42356