HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem syli 54
Description: Syllogism inference with common nested antecedent.
Hypotheses
Ref Expression
syli.1 |- (ps -> (ph -> ch))
syli.2 |- (ch -> (ph -> th))
Assertion
Ref Expression
syli |- (ps -> (ph -> th))
Proof of Theorem syli
StepHypRef Expression
1 syli.1 . 2 |- (ps -> (ph -> ch))
2 syli.2 . . 3 |- (ch -> (ph -> th))
32com12 11 . 2 |- (ph -> (ch -> th))
41, 3sylcom 51 1 |- (ps -> (ph -> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  pclem6 739  onminex 3010  elreldm 3327  tz6.12c 3725  oeordi 4198  f1domg 4377  f1dom2g 4378  ssdom2g 4390  php 4493  cardmin 4832  carduniima 4862  suplem2pr 5134  supsr 5203  elghomlem2 10288
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain