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

Theorem syl6ss 3516
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 3514 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  difss2  3633  rintn0  4416  eqbrrdva  5172  ssxpb  5441  relfld  5533  funssxp  5744  dff2  6033  dff3  6034  fliftf  6201  1stcof  6812  2ndcof  6813  nnunifi  7771  elfiun  7890  marypha1lem  7893  marypha1  7894  ordtypelem7  7949  tcmin  8172  unwf  8228  rankfu  8295  tcrank  8302  aceq3lem  8501  dfac12lem2  8524  ackbij1lem9  8608  ackbij1lem10  8609  ackbij1lem16  8615  fin23lem26  8705  fin23lem27  8708  fin1a2lem6  8785  itunitc  8801  axdc3lem2  8831  ttukeylem5  8893  fpwwe2lem13  9020  canthwelem  9028  pwfseqlem4  9040  wunex2  9116  wunex3  9119  inar1  9153  inatsk  9156  gruina  9196  suprfinzcl  10975  suprzub  11173  uzsupss  11174  uzwo3  11177  rpnnen1lem4  11211  rpnnen1lem5  11212  supxrre  11519  infmxrre  11527  ioodisj  11650  supicclub2  11671  fzossnn0  11824  elfzom1elp1fzo  11851  injresinjlem  11893  uzindi  12059  ssnn0fi  12062  seqcoll  12478  seqcoll2  12479  limsupval2  13266  limsupgre  13267  limsupbnd2  13269  rlimuni  13336  rlimcld2  13364  rlimno1  13439  isercolllem2  13451  isercoll  13453  summolem2a  13500  summolem2  13501  fsumsers  13513  fsumcvg3  13514  4sqlem11  14332  vdwlem8  14365  vdwlem11  14368  ramub2  14391  0ram  14397  0ram2  14398  0ramcl  14400  ramub1lem2  14404  isohom  15027  funcres2c  15128  resscntz  16174  cntzidss  16180  cntzmhm2  16182  pgpssslw  16440  cntzspan  16653  gsumval3OLD  16711  gsumval3  16714  gsum2d  16802  gsum2dOLD  16803  dprdspan  16876  lssintcl  17410  lbsextlem2  17605  lbsextlem3  17606  lbsextlem4  17607  mplbas2  17933  mplbas2OLD  17934  islinds3  18664  fctop  19299  cctop  19301  neitr  19475  ordtbas2  19486  ordtopn1  19489  ordtopn2  19490  lmss  19593  clscon  19725  2ndcdisj  19751  2ndcomap  19753  ptbasfi  19845  txcmplem2  19906  hausdiag  19909  txkgen  19916  basqtop  19975  alexsubb  20309  alexsubALTlem4  20313  tsmsresOLD  20408  tsmsres  20409  tsmsxplem1  20418  tsmsxp  20420  ustrel  20477  utop3cls  20517  prdsmet  20636  metustrelOLD  20821  metustrel  20822  icccmplem2  21091  xrge0tsms  21102  cnmptre  21190  icchmeo  21204  bndth  21221  lebnumlem2  21225  cfilresi  21497  causs  21500  bcthlem5  21530  evthicc  21634  ovolficcss  21644  ovolmge0  21651  ovolgelb  21654  ovollb2lem  21662  ovollb2  21663  ovolunlem1a  21670  ovolunlem1  21671  ovoliunlem1  21676  ovoliunlem2  21677  ovoliun  21679  ovolscalem1  21687  ovolicc1  21690  ovolicc2lem4  21694  ovolicc2  21696  voliunlem2  21724  voliunlem3  21725  ioombl1lem2  21732  ioombl1lem4  21734  uniioovol  21751  uniiccvol  21752  uniioombllem1  21753  uniioombllem2  21755  uniioombllem3  21757  uniioombllem4  21758  uniioombllem6  21760  dyadmbllem  21771  dyadmbl  21772  volcn  21778  vitalilem4  21783  vitalilem5  21784  cnmbf  21829  i1fmul  21866  itg1addlem4  21869  itg2seq  21912  dvbssntr  22067  dvreslem  22076  dvcjbr  22115  dvferm1  22149  dvferm2  22151  cmvth  22155  dvlip  22157  lhop1lem  22177  lhop2  22179  lhop  22180  dvcnvrelem2  22182  dvcnvre  22183  dvfsumle  22185  dvfsumge  22186  dvfsumabs  22187  dvfsumlem2  22191  ftc1a  22201  ftc1lem3  22202  ftc1lem6  22205  itgsubstlem  22212  mdegleb  22227  mdeglt  22228  mdegldg  22229  mdegxrcl  22230  mdegcl  22232  deg1mul3le  22280  ig1pdvds  22340  plyeq0lem  22370  aannenlem2  22487  aalioulem3  22492  taylf  22518  taylthlem2  22531  pserulm  22579  psercn2  22580  psercn  22583  reeff1olem  22603  efcvx  22606  loglesqrt  22888  rlimcnp  23051  xrlimcnp  23054  jensen  23074  wilthlem2  23099  vmadivsumb  23424  pntrsumo1  23506  pntlem3  23550  perpln2  23824  axcontlem10  23980  usgraexmpl  24105  nmoxr  25385  nmooge0  25386  nmoolb  25390  nmoubi  25391  ubthlem1  25490  shmodi  26012  nmopxr  26489  nmfnxr  26502  nmoplb  26530  nmopub  26531  nmfnlb  26547  nmfnleub  26548  nmopun  26637  branmfn  26728  mdslj1i  26942  hatomistici  26985  suppss2f  27178  xppreima2  27188  fpwrelmap  27256  fzssnn  27291  xrge0tsmsd  27466  metideq  27536  metider  27537  pstmfval  27539  sigaclci  27800  insiga  27805  eulerpartlemgs2  27987  ballotlemsima  28122  signsply0  28176  rescon  28359  cvmliftlem8  28405  cvmlift3lem6  28437  prodmolem2a  28671  prodmolem2  28672  zprod  28674  nofulllem5  29071  heicant  29654  mblfinlem2  29657  mblfinlem3  29658  mblfinlem4  29659  ismblfin  29660  itg2gt0cn  29675  ftc1cnnc  29694  ftc1anclem3  29697  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703  areacirclem2  29713  areacirclem3  29714  areacirclem4  29715  ivthALT  29758  neibastop1  29808  topjoin  29814  totbndbnd  29916  prdsbnd  29920  heiborlem1  29938  rrnequiv  29962  reheibor  29966  iccbnd  29967  rmxyelqirr  30478  ttac  30610  hbtlem6  30710  hbt  30711  itgpowd  30815  limcleqr  31214  ibliccsinexp  31296  iblioosinexp  31298  itgiccshift  31326  itgperiod  31327  itgsbtaddcnst  31328  stoweidlem34  31362  stoweidlem59  31387  dirkeritg  31430  fourierdlem31  31466  fourierdlem46  31481  fourierdlem52  31487  fourierdlem53  31488  fourierdlem60  31495  fourierdlem61  31496  fourierdlem62  31497  fourierdlem68  31503  fourierdlem76  31511  fourierdlem85  31520  fourierdlem88  31523  fourierdlem103  31538  fourierdlem104  31539  fouriersw  31560  bnj1145  33146  bnj1137  33148  bnj1136  33150  pmapssbaN  34574  2polssN  34729  paddunN  34741  poldmj1N  34742  ispsubcl2N  34761  psubclinN  34762  paddatclN  34763  poml4N  34767  diaglbN  35870  diaintclN  35873  dibglbN  35981  dibintclN  35982  dicssdvh  36001  dihvalrel  36094  dochexmidlem4  36278  cnvtrrel  36810  rp-imass  36814
  Copyright terms: Public domain W3C validator