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

Theorem syldanl 602
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 413 . . 3 (𝜑 → (𝜓𝜒))
32imdistani 569 . 2 ((𝜑𝜓) → (𝜑𝜒))
4 syldanl.2 . 2 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
53, 4sylan 580 1 (((𝜑𝜓) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  sylanl2  679  oen0  8585  oeordsuc  8593  erth  8751  phplem2  9207  lo1bdd2  15467  grplmulf1o  18896  grplactcnv  18925  trust  23733  efrlim  26471  fedgmullem2  32710  submateq  32784  heibor1lem  36672  idlnegcl  36885  igenmin  36927  eqvrelth  37476  sticksstones22  40979  binomcxplemnotnn0  43105  vonioolem1  45386  vonicclem1  45389  smfsuplem1  45517  smflimsuplem4  45529
  Copyright terms: Public domain W3C validator