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

Theorem sylan9 657
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
sylan9.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylan9.2  |-  ( th 
->  ( ch  ->  ta ) )
Assertion
Ref Expression
sylan9  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )

Proof of Theorem sylan9
StepHypRef Expression
1 sylan9.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylan9.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
31, 2syl9 71 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 429 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  sbal1OLD  2172  rspc2  3099  rspc3v  3103  trintss  4422  copsexg  4597  copsexgOLD  4598  chfnrn  5835  fvcofneq  5872  ffnfv  5890  f1elima  5997  onint  6427  peano5  6520  f1oweALT  6582  smoel2  6845  th3q  7230  pssnn  7552  fiint  7609  dffi2  7694  alephnbtwn  8262  cfcof  8464  zorn2lem7  8692  suplem1pr  9242  cau3lem  12863  divalglem8  13625  efgi  16237  elfrlmbasn0  18212  tx1stc  19245  fbunfip  19464  filuni  19480  ufileu  19514  rescncf  20495  shmodsi  24814  spanuni  24969  spansneleq  24995  mdi  25721  dmdi  25728  dmdi4  25733  funimass4f  25973  locfincmp  28602  ffnafv  30103  bj-ax89  32270
  Copyright terms: Public domain W3C validator