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

Theorem sylan9 655
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 70 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 427 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  rspc2  3167  rspc3v  3171  trintss  4504  copsexg  4675  chfnrn  5975  fvcofneq  6016  ffnfv  6035  f1elima  6151  onint  6612  peano5  6706  f1oweALT  6767  smoel2  7066  pssnn  7772  fiint  7830  dffi2  7916  alephnbtwn  8483  cfcof  8685  zorn2lem7  8913  suplem1pr  9459  addsrpr  9481  mulsrpr  9482  cau3lem  13334  divalglem8  14265  efgi  17059  elfrlmbasn0  19090  locfincmp  20317  tx1stc  20441  fbunfip  20660  filuni  20676  ufileu  20710  rescncf  21691  shmodsi  26707  spanuni  26862  spansneleq  26888  mdi  27613  dmdi  27620  dmdi4  27625  funimass4f  27903  bj-ax89  30789  ffnafv  37605
  Copyright terms: Public domain W3C validator