MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syldanl Structured version   Visualization version   GIF version

Theorem syldanl 603
Description: A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.)
Hypotheses
Ref Expression
syldanl.1 ((𝜑𝜓) → 𝜒)
syldanl.2 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
syldanl (((𝜑𝜓) ∧ 𝜃) → 𝜏)

Proof of Theorem syldanl
StepHypRef Expression
1 syldanl.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 414 . . 3 (𝜑 → (𝜓𝜒))
32imdistani 570 . 2 ((𝜑𝜓) → (𝜑𝜒))
4 syldanl.2 . 2 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
53, 4sylan 581 1 (((𝜑𝜓) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  sylanl2  680  oen0  8537  oeordsuc  8545  erth  8703  phplem2  9158  lo1bdd2  15415  grplmulf1o  18829  grplactcnv  18858  trust  23604  efrlim  26342  fedgmullem2  32389  submateq  32454  heibor1lem  36318  idlnegcl  36531  igenmin  36573  eqvrelth  37123  sticksstones22  40626  binomcxplemnotnn0  42728  vonioolem1  45011  vonicclem1  45014  smfsuplem1  45142  smflimsuplem4  45154
  Copyright terms: Public domain W3C validator