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  1958  limsssuc  6561  tfindsg  6571  findsg  6603  f1oweALT  6661  oaordi  7085  pssnn  7632  inf3lem2  7936  cardlim  8243  ac10ct  8305  cardaleph  8360  cfub  8519  cfcoflem  8542  hsmexlem2  8697  zorn2lem7  8772  pwcfsdom  8848  grur1a  9087  genpcd  9276  supmul  10399  zeo  10828  uzwo  11018  uzwoOLD  11019  xrub  11375  iccsupr  11483  climuni  13132  efgi2  16326  opnnei  18840  tgcn  18972  uffix  19610  alexsubALTlem2  19736  alexsubALT  19739  metrest  20215  causs  20925  subgoablo  23933  ocin  24834  spanuni  25082  superpos  25893  3orel13  27507  trpredmintr  27829  frmin  27837  nndivsub  28437  supadd  28556  locfincf  28716  cover2  28745  metf1o  28789  stoweidlem62  29995  bnj518  32179  bj-spimtv  32514
  Copyright terms: Public domain W3C validator