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  1989  limsssuc  6666  tfindsg  6676  findsg  6708  f1oweALT  6765  oaordi  7193  pssnn  7736  inf3lem2  8044  cardlim  8351  ac10ct  8413  cardaleph  8468  cfub  8627  cfcoflem  8650  hsmexlem2  8805  zorn2lem7  8880  pwcfsdom  8956  grur1a  9195  genpcd  9382  supmul  10512  zeo  10949  uzwo  11148  uzwoOLD  11149  xrub  11507  iccsupr  11621  reuccats1lem  12679  climuni  13349  efgi2  16612  opnnei  19487  tgcn  19619  locfincf  19898  uffix  20288  alexsubALTlem2  20414  alexsubALT  20417  metrest  20893  causs  21603  subgoablo  25178  ocin  26079  spanuni  26327  superpos  27138  3orel13  28960  trpredmintr  29282  frmin  29290  nndivsub  29890  supadd  30010  cover2  30172  metf1o  30216  stoweidlem62  31729  bnj518  33651  bj-spimtv  33992
  Copyright terms: Public domain W3C validator