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

Theorem syldanl 604
 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 416 . . 3 (𝜑 → (𝜓𝜒))
32imdistani 572 . 2 ((𝜑𝜓) → (𝜑𝜒))
4 syldanl.2 . 2 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
53, 4sylan 583 1 (((𝜑𝜓) ∧ 𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  sylanl2  680  oen0  8209  oeordsuc  8217  erth  8335  lo1bdd2  14884  grplmulf1o  18176  grplactcnv  18205  trust  22841  efrlim  25561  fedgmullem2  31089  submateq  31137  heibor1lem  35193  idlnegcl  35406  igenmin  35448  eqvrelth  35952  binomcxplemnotnn0  40981  vonioolem1  43246  vonicclem1  43249  smfsuplem1  43369  smflimsuplem4  43381
 Copyright terms: Public domain W3C validator