MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl9 Unicode version

Theorem syl9 66
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Hypotheses
Ref Expression
syl9.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl9.2  |-  ( th 
->  ( ch  ->  ta ) )
Assertion
Ref Expression
syl9  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )

Proof of Theorem syl9
StepHypRef Expression
1 syl9.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl9.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
32a1i 10 . 2  |-  ( ph  ->  ( th  ->  ( ch  ->  ta ) ) )
41, 3syl5d 62 1  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl9r  67  com23  72  sylan9  638  19.21t  1802  sbequi  2012  sbal1  2078  reuss2  3461  reupick  3465  ordtr2  4452  suc11  4512  elres  5006  funimass4  5589  fliftfun  5827  tfrlem1  6407  omlimcl  6592  nneob  6666  rankwflemb  7481  cflm  7892  domtriomlem  8084  grothomex  8467  sup3  9727  caubnd  11858  spwmo  14351  fbflim2  17688  ellimc3  19245  dfon2lem6  24215  svs2  25590  cmptdst  25671  propsrc  25971  isibg2aa  26215  bsstr  26231  nbssntr  26232  abhp  26276  opnrebl2  26339  pm11.71  27699  ax10ext  27709  3cyclfrgrarn1  28435  sbequiNEW7  29553  sbal1NEW7  29587  diaintclN  31870  dibintclN  31979  dihintcl  32156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator