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

Theorem syl9 71
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-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 11 . 2  |-  ( ph  ->  ( th  ->  ( ch  ->  ta ) ) )
41, 3syl5d 67 1  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl9r  72  com23  78  sylan9  657  19.21t  1852  axc9lem1  1970  axc9lem2  2013  axc11n  2022  axc11nOLD  2023  sbequi  2089  sbal1OLD  2194  reuss2  3778  reupick  3782  ordtr2  4922  suc11  4981  elres  5307  funimass4  5916  fliftfun  6196  omlimcl  7224  nneob  7298  rankwflemb  8207  cflm  8626  domtriomlem  8818  grothomex  9203  sup3  10496  caubnd  13147  fbflim2  20210  ellimc3  22015  3cyclfrgrarn1  24685  dfon2lem6  28794  opnrebl2  29714  pm11.71  30881  axc11next  30891  bj-axc11nv  33397  stdpc5t  33481  diaintclN  35855  dibintclN  35964  dihintcl  36141
  Copyright terms: Public domain W3C validator