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

Theorem sylan9r 662
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 74 . 2  |-  ( th 
->  ( ph  ->  ( ps  ->  ta ) ) )
43imp 430 1  |-  ( ( th  /\  ph )  ->  ( ps  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  spimt  2058  limsssuc  6682  tfindsg  6692  findsg  6725  f1oweALT  6782  oaordi  7246  pssnn  7787  inf3lem2  8125  cardlim  8396  ac10ct  8454  cardaleph  8509  cfub  8668  cfcoflem  8691  hsmexlem2  8846  zorn2lem7  8921  pwcfsdom  8997  grur1a  9233  genpcd  9420  supadd  10564  supmul  10568  zeo  11010  uzwo  11211  xrub  11586  iccsupr  11716  reuccats1lem  12810  climuni  13583  efgi2  17303  opnnei  20060  tgcn  20192  locfincf  20470  uffix  20860  alexsubALTlem2  20987  alexsubALT  20990  metrest  21463  causs  22154  subgoablo  25881  ocin  26781  spanuni  27029  superpos  27839  bnj518  29482  3orel13  30134  trpredmintr  30256  frmin  30264  nndivsub  30899  bj-spimtv  31055  cover2  31744  metf1o  31788  stoweidlem62  37496  stoweidlem62OLD  37497  reuccatpfxs1lem  38377
  Copyright terms: Public domain W3C validator