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  1999  limsssuc  4641  tfindsg  4651  findsg  4683  f1oweALT  5851  oaordi  6544  pssnn  7081  inf3lem2  7330  cardlim  7605  ac10ct  7661  cardaleph  7716  cfub  7875  cfcoflem  7898  hsmexlem2  8053  zorn2lem7  8129  pwcfsdom  8205  grur1a  8441  genpcd  8630  supmul  9722  zeo  10097  uzwo  10281  uzwoOLD  10282  xrub  10630  iccsupr  10736  climuni  12026  efgi2  15034  opnnei  16857  tgcn  16982  uffix  17616  alexsubALTlem2  17742  alexsubALT  17745  metrest  18070  causs  18724  subgoablo  20978  ocin  21875  spanuni  22123  superpos  22934  3orel13  24071  trpredmintr  24234  frmin  24242  nndivsub  24896  untind  25018  prodeq3ii  25308  locfincf  26306  cover2  26358  metf1o  26469  bnj518  28918  a12studyALT  29133
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