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

Theorem sylan9r 640
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 69 . 2  |-  ( th 
->  ( ph  ->  ( ps  ->  ta ) ) )
43imp 419 1  |-  ( ( th  /\  ph )  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  spimt  1955  sbequiOLD  2114  limsssuc  4830  tfindsg  4840  findsg  4872  f1oweALT  6074  oaordi  6789  pssnn  7327  inf3lem2  7584  cardlim  7859  ac10ct  7915  cardaleph  7970  cfub  8129  cfcoflem  8152  hsmexlem2  8307  zorn2lem7  8382  pwcfsdom  8458  grur1a  8694  genpcd  8883  supmul  9976  zeo  10355  uzwo  10539  uzwoOLD  10540  xrub  10890  iccsupr  10997  climuni  12346  efgi2  15357  opnnei  17184  tgcn  17316  uffix  17953  alexsubALTlem2  18079  alexsubALT  18082  metrest  18554  causs  19251  subgoablo  21899  ocin  22798  spanuni  23046  superpos  23857  3orel13  25174  trpredmintr  25509  frmin  25517  nndivsub  26207  supadd  26238  locfincf  26386  cover2  26415  metf1o  26461  stoweidlem62  27787  bnj518  29257  sbequiNEW7  29579
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 178  df-an 361
  Copyright terms: Public domain W3C validator