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  1790  sbequi  1999  sbal1  2065  reuss2  3448  reupick  3452  ordtr2  4436  suc11  4496  elres  4990  funimass4  5573  fliftfun  5811  tfrlem1  6391  omlimcl  6576  nneob  6650  rankwflemb  7465  cflm  7876  domtriomlem  8068  grothomex  8451  sup3  9711  caubnd  11842  spwmo  14335  fbflim2  17672  ellimc3  19229  dfon2lem6  24144  svs2  25487  cmptdst  25568  propsrc  25868  isibg2aa  26112  bsstr  26128  nbssntr  26129  abhp  26173  opnrebl2  26236  pm11.71  27596  ax10ext  27606  diaintclN  31248  dibintclN  31357  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator