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

Theorem sylan9 638
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-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 66 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 418 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sbequi  2064  sbal1  2131  rspc2  2965  rspc3v  2969  trintss  4210  copsexg  4334  onint  4668  peano5  4761  chfnrn  5719  ffnfv  5768  f1elima  5874  f1oweALT  5938  smoel2  6467  th3q  6855  pssnn  7169  fiint  7223  dffi2  7266  alephnbtwn  7788  cfcof  7990  zorn2lem7  8219  suplem1pr  8766  cau3lem  11934  divalglem8  12696  efgi  15127  tx1stc  17450  fbunfip  17666  filuni  17682  ufileu  17716  rescncf  18504  shmodsi  22082  spanuni  22237  spansneleq  22263  mdi  22989  dmdi  22996  dmdi4  23001  funimass4f  23248  locfincmp  25628  ffnafv  27359  sbequiNEW7  28999  sbal1NEW7  29033  a12study  29201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator