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

Theorem sylan9r 639
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-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 67 . 2  |-  ( th 
->  ( ph  ->  ( ps  ->  ta ) ) )
43imp 418 1  |-  ( ( th  /\  ph )  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sbequi  2012  limsssuc  4657  tfindsg  4667  findsg  4699  f1oweALT  5867  oaordi  6560  pssnn  7097  inf3lem2  7346  cardlim  7621  ac10ct  7677  cardaleph  7732  cfub  7891  cfcoflem  7914  hsmexlem2  8069  zorn2lem7  8145  pwcfsdom  8221  grur1a  8457  genpcd  8646  supmul  9738  zeo  10113  uzwo  10297  uzwoOLD  10298  xrub  10646  iccsupr  10752  climuni  12042  efgi2  15050  opnnei  16873  tgcn  16998  uffix  17632  alexsubALTlem2  17758  alexsubALT  17761  metrest  18086  causs  18740  subgoablo  20994  ocin  21891  spanuni  22139  superpos  22950  3orel13  24086  trpredmintr  24305  frmin  24313  nndivsub  24968  supadd  24996  untind  25121  prodeq3ii  25411  locfincf  26409  cover2  26461  metf1o  26572  bnj518  29234  sbequiNEW7  29553  a12studyALT  29755
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