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

Theorem syl9 72
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 68 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  73  com23  80  sylan9  669  19.21t  2006  axc9lem1  2106  axc9lem2  2146  axc9lem2OLD  2147  axc11n  2157  axc11nOLD  2158  axc11nALT  2159  sbequi  2224  reuss2  3714  reupick  3718  elres  5146  ordtr2  5474  suc11  5533  funimass4  5930  fliftfun  6223  omlimcl  7297  nneob  7371  rankwflemb  8282  cflm  8698  domtriomlem  8890  grothomex  9272  sup3  10588  caubnd  13498  fbflim2  21070  ellimc3  22913  3cyclfrgrarn1  25819  dfon2lem6  30505  opnrebl2  31048  bj-axc11nv  31414  stdpc5t  31495  diaintclN  34697  dibintclN  34806  dihintcl  34983  pm11.71  36817  axc11next  36827  usgruspgrb  39429  usgredgsscusgredg  39685
  Copyright terms: Public domain W3C validator