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

Theorem sylan9r 658
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
sylan9r.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylan9r.2  |-  ( th 
->  ( ch  ->  ta ) )
Assertion
Ref Expression
sylan9r  |-  ( ( th  /\  ph )  ->  ( ps  ->  ta ) )

Proof of Theorem sylan9r
StepHypRef Expression
1 sylan9r.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylan9r.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
31, 2syl9r 72 . 2  |-  ( th 
->  ( ph  ->  ( ps  ->  ta ) ) )
43imp 429 1  |-  ( ( th  /\  ph )  ->  ( 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:  spimt  1967  limsssuc  6656  tfindsg  6666  findsg  6698  f1oweALT  6758  oaordi  7185  pssnn  7728  inf3lem2  8035  cardlim  8342  ac10ct  8404  cardaleph  8459  cfub  8618  cfcoflem  8641  hsmexlem2  8796  zorn2lem7  8871  pwcfsdom  8947  grur1a  9186  genpcd  9373  supmul  10500  zeo  10935  uzwo  11133  uzwoOLD  11134  xrub  11492  iccsupr  11606  climuni  13324  efgi2  16532  opnnei  19380  tgcn  19512  uffix  20150  alexsubALTlem2  20276  alexsubALT  20279  metrest  20755  causs  21465  subgoablo  24839  ocin  25740  spanuni  25988  superpos  26799  3orel13  28419  trpredmintr  28741  frmin  28749  nndivsub  29349  supadd  29469  locfincf  29629  cover2  29658  metf1o  29702  stoweidlem62  31181  bnj518  32898  bj-spimtv  33235
  Copyright terms: Public domain W3C validator