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

Theorem syldanl 601
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 412 . . 3 (𝜑 → (𝜓𝜒))
32imdistani 568 . 2 ((𝜑𝜓) → (𝜑𝜒))
4 syldanl.2 . 2 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
53, 4sylan 579 1 (((𝜑𝜓) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 396
This theorem is referenced by:  sylanl2  678  oen0  8582  oeordsuc  8590  erth  8749  phplem2  9205  lo1bdd2  15466  grplmulf1o  18934  grplactcnv  18963  trust  24058  efrlim  26820  efrlimOLD  26821  fedgmullem2  33197  submateq  33281  heibor1lem  37171  idlnegcl  37384  igenmin  37426  eqvrelth  37975  sticksstones22  41481  binomcxplemnotnn0  43629  vonioolem1  45906  vonicclem1  45909  smfsuplem1  46037  smflimsuplem4  46049
  Copyright terms: Public domain W3C validator