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  1999  sbal1  2065  rspc2  2889  rspc3v  2893  trintss  4129  copsexg  4252  onint  4586  peano5  4679  chfnrn  5636  ffnfv  5685  f1elima  5787  f1oweALT  5851  smoel2  6380  th3q  6767  pssnn  7081  fiint  7133  dffi2  7176  alephnbtwn  7698  cfcof  7900  zorn2lem7  8129  suplem1pr  8676  cau3lem  11838  divalglem8  12599  efgi  15028  tx1stc  17344  fbunfip  17564  filuni  17580  ufileu  17614  rescncf  18401  shmodsi  21968  spanuni  22123  spansneleq  22149  mdi  22875  dmdi  22882  dmdi4  22887  funimass4f  23042  locfincmp  26304  ffnafv  28033  a12study  29132
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