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  8588  oeordsuc  8596  erth  8754  phplem2  9210  lo1bdd2  15472  grplmulf1o  18933  grplactcnv  18962  trust  23954  efrlim  26698  fedgmullem2  32991  submateq  33075  heibor1lem  36980  idlnegcl  37193  igenmin  37235  eqvrelth  37784  sticksstones22  41290  binomcxplemnotnn0  43417  vonioolem1  45695  vonicclem1  45698  smfsuplem1  45826  smflimsuplem4  45838
  Copyright terms: Public domain W3C validator