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

Theorem syl6ss 3476
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 3474 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  difss2  3594  rintn0  4393  eqbrrdva  5023  ssxpb  5290  relfld  5380  funssxp  5759  dff2  6049  dff3  6050  fliftf  6223  1stcof  6835  2ndcof  6836  nnunifi  7831  elfiun  7953  marypha1lem  7956  marypha1  7957  ordtypelem7  8048  tcmin  8233  unwf  8289  rankfu  8356  tcrank  8363  aceq3lem  8558  dfac12lem2  8581  ackbij1lem9  8665  ackbij1lem10  8666  ackbij1lem16  8672  fin23lem26  8762  fin23lem27  8765  fin1a2lem6  8842  itunitc  8858  axdc3lem2  8888  ttukeylem5  8950  fpwwe2lem13  9074  canthwelem  9082  pwfseqlem4  9094  wunex2  9170  wunex3  9173  inar1  9207  inatsk  9210  gruina  9250  suprfinzcl  11057  suprzub  11262  uzsupss  11263  uzwo3  11266  rpnnen1lem4  11300  rpnnen1lem5  11301  supxrre  11620  infxrre  11629  infmxrreOLD  11633  ioodisj  11769  supicclub2  11790  fzssnn  11849  fzossnn0  11956  elfzom1elp1fzo  11987  injresinjlem  12030  uzindi  12200  ssnn0fi  12203  seqcoll  12631  seqcoll2  12632  reltrclfv  13081  relexpdmg  13105  relexpdm  13106  relexprng  13109  relexprn  13110  relexpfld  13112  relexpaddg  13116  limsupval2  13539  limsupval2OLD  13540  limsupgre  13541  limsupgreOLD  13542  limsupbnd2  13545  limsupbnd2OLD  13546  rlimuni  13613  rlimcld2  13641  rlimno1  13716  isercolllem2  13728  isercoll  13730  summolem2a  13780  summolem2  13781  fsumsers  13793  fsumcvg3  13794  prodmolem2a  13987  prodmolem2  13988  zprod  13990  lcmscllemOLD  14581  lcmfnnval  14593  lcmfnnvalOLD  14596  lcmfnncl  14601  4sqlem11  14898  vdwlem8  14937  vdwlem11  14940  ramub2  14970  0ram  14977  0ram2  14978  0ramcl  14980  ramub1lem2  14984  prmgaplem3  15022  prmgaplem4  15023  isohom  15680  funcres2c  15805  resscntz  16984  cntzidss  16990  cntzmhm2  16992  pgpssslw  17265  cntzspan  17481  gsumval3  17540  gsum2d  17603  dprdspan  17659  dprdres  17660  lssintcl  18186  lbsextlem2  18381  lbsextlem3  18382  lbsextlem4  18383  mplbas2  18693  islinds3  19390  fctop  20017  cctop  20019  neitr  20194  ordtbas2  20205  ordtopn1  20208  ordtopn2  20209  lmss  20312  clscon  20443  2ndcdisj  20469  2ndcomap  20471  ptbasfi  20594  txcmplem2  20655  hausdiag  20658  txkgen  20665  basqtop  20724  alexsubb  21059  alexsubALTlem4  21063  tsmsres  21156  tsmsxplem1  21165  tsmsxp  21167  ustrel  21224  utop3cls  21264  prdsmet  21383  metustrel  21565  icccmplem2  21839  xrge0tsms  21850  cnmptre  21953  icchmeo  21967  bndth  21984  lebnumlem2  21988  lebnumlem2OLD  21991  cfilresi  22263  causs  22266  bcthlem5  22294  evthicc  22408  ovolficcss  22420  ovolmge0  22428  ovolgelb  22431  ovollb2lem  22439  ovollb2  22440  ovolunlem1a  22447  ovolunlem1  22448  ovoliunlem1  22453  ovoliunlem2  22454  ovoliun  22456  ovolscalem1  22464  ovolicc1  22467  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2  22474  voliunlem2  22502  voliunlem3  22503  ioombl1lem2  22510  ioombl1lem4  22512  uniioovol  22534  uniiccvol  22535  uniioombllem1  22536  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem3  22541  uniioombllem4  22542  uniioombllem6  22544  dyadmbllem  22555  dyadmbl  22556  volcn  22562  vitalilem4  22567  vitalilem5  22568  cnmbf  22613  i1fmul  22652  itg1addlem4  22655  itg2seq  22698  dvbssntr  22853  dvreslem  22862  dvcjbr  22901  dvferm1  22935  dvferm2  22937  cmvth  22941  dvlip  22943  lhop1lem  22963  lhop2  22965  lhop  22966  dvcnvrelem2  22968  dvcnvre  22969  dvfsumle  22971  dvfsumge  22972  dvfsumabs  22973  dvfsumlem2  22977  ftc1a  22987  ftc1lem3  22988  ftc1lem6  22991  itgsubstlem  22998  mdegleb  23011  mdeglt  23012  mdegldg  23013  mdegxrcl  23014  mdegcl  23016  deg1mul3le  23063  ig1pdvds  23126  ig1pdvdsOLD  23132  plyeq0lem  23162  aannenlem2  23283  aalioulem3  23288  taylf  23314  taylthlem2  23327  pserulm  23375  psercn2  23376  psercn  23379  reeff1olem  23399  efcvx  23402  loglesqrt  23696  rlimcnp  23889  xrlimcnp  23892  jensen  23912  wilthlem2  23992  vmadivsumb  24319  pntrsumo1  24401  pntlem3  24445  perpln2  24754  axcontlem10  25001  usgraexmplef  25126  nmoxr  26405  nmooge0  26406  nmoolb  26410  nmoubi  26411  ubthlem1  26510  shmodi  27041  nmopxr  27517  nmfnxr  27530  nmoplb  27558  nmopub  27559  nmfnlb  27575  nmfnleub  27576  nmopun  27665  branmfn  27756  mdslj1i  27970  hatomistici  28013  suppss2fOLD  28239  xppreima2  28251  fpwrelmap  28324  infxrge0gelb  28356  infxrge0gelbOLD  28357  xrge0tsmsd  28556  metideq  28704  metider  28705  pstmfval  28707  esumgect  28919  esum2d  28922  sigaclci  28962  insiga  28967  omssubadd  29136  omssubaddOLD  29140  eulerpartlemgs2  29221  ballotlemsima  29356  ballotlemsimaOLD  29394  signsply0  29448  bnj1145  29810  bnj1137  29812  bnj1136  29814  rescon  29977  cvmliftlem8  30023  cvmlift3lem6  30055  mclsssvlem  30208  mclsind  30216  mclsppslem  30229  nofulllem5  30600  ivthALT  30996  neibastop1  31020  topjoin  31026  ptrecube  31904  poimirlem6  31910  poimirlem15  31919  heicant  31939  mblfinlem2  31942  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  itg2gt0cn  31961  ftc1cnnc  31980  ftc1anclem3  31983  ftc1anclem7  31987  ftc1anclem8  31988  ftc1anc  31989  areacirclem2  31997  areacirclem3  31998  areacirclem4  31999  totbndbnd  32085  prdsbnd  32089  heiborlem1  32107  rrnequiv  32131  reheibor  32135  iccbnd  32136  pmapssbaN  33294  2polssN  33449  paddunN  33461  poldmj1N  33462  ispsubcl2N  33481  psubclinN  33482  paddatclN  33483  poml4N  33487  diaglbN  34592  diaintclN  34595  dibglbN  34703  dibintclN  34704  dicssdvh  34723  dihvalrel  34816  dochexmidlem4  35000  rmxyelqirr  35728  ttac  35861  hbtlem6  35958  hbt  35959  itgpowd  36069  cnvssb  36162  cnvrcl0  36202  cnvtrrel  36232  relexpaddss  36280  cotrcltrcl  36287  cotrclrcl  36304  frege96d  36311  frege97d  36314  frege109d  36319  frege131d  36326  rp-imass  36336  uzfissfz  37503  suplesup  37516  limciccioolb  37641  limcicciooub  37657  limcleqr  37665  cncfiooicclem1  37711  ibliccsinexp  37767  iblioosinexp  37769  itgcoscmulx  37786  itgsincmulx  37791  itgsubsticclem  37792  itgiccshift  37797  itgperiod  37798  itgsbtaddcnst  37799  stoweidlem34  37835  stoweidlem59  37860  dirkeritg  37904  dirkercncflem2  37906  fourierdlem20  37929  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem39  37949  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem46  37956  fourierdlem52  37962  fourierdlem53  37963  fourierdlem60  37970  fourierdlem61  37971  fourierdlem62  37972  fourierdlem68  37978  fourierdlem76  37986  fourierdlem85  37995  fourierdlem88  37998  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem93  38003  fourierdlem94  38004  fourierdlem103  38013  fourierdlem104  38014  fourierdlem111  38021  fouriersw  38035  etransclem46  38085  etransclem48OLD  38087  etransclem48  38088  sge0less  38142  sge0resplit  38156  sge0isum  38177  iccpartipre  38605  bgoldbtbndlem2  38771
  Copyright terms: Public domain W3C validator