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

Theorem sylan9r 656
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 427 1  |-  ( ( th  /\  ph )  ->  ( ps  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  spimt  2010  limsssuc  6658  tfindsg  6668  findsg  6700  f1oweALT  6757  oaordi  7187  pssnn  7731  inf3lem2  8037  cardlim  8344  ac10ct  8406  cardaleph  8461  cfub  8620  cfcoflem  8643  hsmexlem2  8798  zorn2lem7  8873  pwcfsdom  8949  grur1a  9186  genpcd  9373  supmul  10506  zeo  10944  uzwo  11145  uzwoOLD  11146  xrub  11506  iccsupr  11620  reuccats1lem  12696  climuni  13457  efgi2  16942  opnnei  19788  tgcn  19920  locfincf  20198  uffix  20588  alexsubALTlem2  20714  alexsubALT  20717  metrest  21193  causs  21903  subgoablo  25511  ocin  26412  spanuni  26660  superpos  27471  3orel13  29335  trpredmintr  29554  frmin  29562  nndivsub  30150  supadd  30282  cover2  30444  metf1o  30488  stoweidlem62  32083  reuccatpfxs1lem  32661  bnj518  34345  bj-spimtv  34679
  Copyright terms: Public domain W3C validator