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

Theorem syl6ss 3389
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl6ss.1  |-  ( ph  ->  A  C_  B )
syl6ss.2  |-  B  C_  C
Assertion
Ref Expression
syl6ss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl6ss
StepHypRef Expression
1 syl6ss.1 . 2  |-  ( ph  ->  A  C_  B )
2 syl6ss.2 . . 3  |-  B  C_  C
32a1i 11 . 2  |-  ( ph  ->  B  C_  C )
41, 3sstrd 3387 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363
This theorem is referenced by:  difss2  3506  rintn0  4282  eqbrrdva  5030  ssxpb  5293  relfld  5384  funssxp  5592  dff2  5876  dff3  5877  fliftf  6029  1stcof  6625  2ndcof  6626  nnunifi  7584  elfiun  7701  marypha1lem  7704  marypha1  7705  ordtypelem7  7759  tcmin  7982  unwf  8038  rankfu  8105  tcrank  8112  aceq3lem  8311  dfac12lem2  8334  ackbij1lem9  8418  ackbij1lem10  8419  ackbij1lem16  8425  fin23lem26  8515  fin23lem27  8518  fin1a2lem6  8595  itunitc  8611  axdc3lem2  8641  ttukeylem5  8703  fpwwe2lem13  8830  canthwelem  8838  pwfseqlem4  8850  wunex2  8926  wunex3  8929  inar1  8963  inatsk  8966  gruina  9006  suprzub  10967  uzsupss  10968  uzwo3  10969  rpnnen1lem4  11003  rpnnen1lem5  11004  supxrre  11311  infmxrre  11319  ioodisj  11436  supicclub2  11457  fzossnn0  11601  injresinjlem  11659  uzindi  11824  seqcoll  12237  seqcoll2  12238  limsupval2  12979  limsupgre  12980  limsupbnd2  12982  rlimuni  13049  rlimcld2  13077  rlimno1  13152  isercolllem2  13164  isercoll  13166  summolem2a  13213  summolem2  13214  fsumsers  13226  fsumcvg3  13227  4sqlem11  14037  vdwlem8  14070  vdwlem11  14073  ramub2  14096  0ram  14102  0ram2  14103  0ramcl  14105  ramub1lem2  14109  isohom  14731  funcres2c  14832  resscntz  15870  cntzidss  15876  cntzmhm2  15878  pgpssslw  16134  cntzspan  16347  gsumval3OLD  16403  gsumval3  16406  gsum2d  16485  gsum2dOLD  16486  dprdspan  16546  lssintcl  17067  lbsextlem2  17262  lbsextlem3  17263  lbsextlem4  17264  mplbas2  17573  mplbas2OLD  17574  islinds3  18285  fctop  18630  cctop  18632  neitr  18806  ordtbas2  18817  ordtopn1  18820  ordtopn2  18821  lmss  18924  clscon  19056  2ndcdisj  19082  2ndcomap  19084  ptbasfi  19176  txcmplem2  19237  hausdiag  19240  txkgen  19247  basqtop  19306  alexsubb  19640  alexsubALTlem4  19644  tsmsresOLD  19739  tsmsres  19740  tsmsxplem1  19749  tsmsxp  19751  ustrel  19808  utop3cls  19848  prdsmet  19967  metustrelOLD  20152  metustrel  20153  icccmplem2  20422  xrge0tsms  20433  cnmptre  20521  icchmeo  20535  bndth  20552  lebnumlem2  20556  cfilresi  20828  causs  20831  bcthlem5  20861  evthicc  20965  ovolficcss  20975  ovolmge0  20982  ovolgelb  20985  ovollb2lem  20993  ovollb2  20994  ovolunlem1a  21001  ovolunlem1  21002  ovoliunlem1  21007  ovoliunlem2  21008  ovoliun  21010  ovolscalem1  21018  ovolicc1  21021  ovolicc2lem4  21025  ovolicc2  21027  voliunlem2  21054  voliunlem3  21055  ioombl1lem2  21062  ioombl1lem4  21064  uniioovol  21081  uniiccvol  21082  uniioombllem1  21083  uniioombllem2  21085  uniioombllem3  21087  uniioombllem4  21088  uniioombllem6  21090  dyadmbllem  21101  dyadmbl  21102  volcn  21108  vitalilem4  21113  vitalilem5  21114  cnmbf  21159  i1fmul  21196  itg1addlem4  21199  itg2seq  21242  dvbssntr  21397  dvreslem  21406  dvcjbr  21445  dvferm1  21479  dvferm2  21481  cmvth  21485  dvlip  21487  lhop1lem  21507  lhop2  21509  lhop  21510  dvcnvrelem2  21512  dvcnvre  21513  dvfsumle  21515  dvfsumge  21516  dvfsumabs  21517  dvfsumlem2  21521  ftc1a  21531  ftc1lem3  21532  ftc1lem6  21535  itgsubstlem  21542  mdegleb  21557  mdeglt  21558  mdegldg  21559  mdegxrcl  21560  mdegcl  21562  deg1mul3le  21610  ig1pdvds  21670  plyeq0lem  21700  aannenlem2  21817  aalioulem3  21822  taylf  21848  taylthlem2  21861  pserulm  21909  psercn2  21910  psercn  21913  reeff1olem  21933  efcvx  21936  loglesqr  22218  rlimcnp  22381  xrlimcnp  22384  jensen  22404  wilthlem2  22429  vmadivsumb  22754  pntrsumo1  22836  pntlem3  22880  axcontlem10  23241  usgraexmpl  23341  nmoxr  24188  nmooge0  24189  nmoolb  24193  nmoubi  24194  ubthlem1  24293  shmodi  24815  nmopxr  25292  nmfnxr  25305  nmoplb  25333  nmopub  25334  nmfnlb  25350  nmfnleub  25351  nmopun  25440  branmfn  25531  mdslj1i  25745  hatomistici  25788  suppss2f  25976  xppreima2  25987  fpwrelmap  26055  fzssnn  26096  xrge0tsmsd  26275  metideq  26342  metider  26343  pstmfval  26345  sigaclci  26597  insiga  26602  eulerpartlemgs2  26785  ballotlemsima  26920  signsply0  26974  rescon  27157  cvmliftlem8  27203  cvmlift3lem6  27235  prodmolem2a  27469  prodmolem2  27470  zprod  27472  nofulllem5  27869  heicant  28452  mblfinlem2  28455  mblfinlem3  28456  mblfinlem4  28457  ismblfin  28458  itg2gt0cn  28473  ftc1cnnc  28492  ftc1anclem3  28495  ftc1anclem7  28499  ftc1anclem8  28500  ftc1anc  28501  areacirclem2  28511  areacirclem3  28512  areacirclem4  28513  ivthALT  28556  neibastop1  28606  topjoin  28612  totbndbnd  28714  prdsbnd  28718  heiborlem1  28736  rrnequiv  28760  reheibor  28764  iccbnd  28765  rmxyelqirr  29277  ttac  29411  hbtlem6  29511  hbt  29512  itgpowd  29616  ibliccsinexp  29817  iblioosinexp  29819  stoweidlem34  29855  stoweidlem59  29880  suprfinzcl  30774  ssnn0fi  30775  bnj1145  32080  bnj1137  32082  bnj1136  32084  pmapssbaN  33500  2polssN  33655  paddunN  33667  poldmj1N  33668  ispsubcl2N  33687  psubclinN  33688  paddatclN  33689  poml4N  33693  diaglbN  34796  diaintclN  34799  dibglbN  34907  dibintclN  34908  dicssdvh  34927  dihvalrel  35020  dochexmidlem4  35204
  Copyright terms: Public domain W3C validator