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

Theorem syl6ss 3356
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 3354 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  difss2  3473  rintn0  4249  eqbrrdva  4996  ssxpb  5260  relfld  5351  funssxp  5559  dff2  5843  dff3  5844  fliftf  5995  1stcof  6593  2ndcof  6594  nnunifi  7551  elfiun  7668  marypha1lem  7671  marypha1  7672  ordtypelem7  7726  tcmin  7949  unwf  8005  rankfu  8072  tcrank  8079  aceq3lem  8278  dfac12lem2  8301  ackbij1lem9  8385  ackbij1lem10  8386  ackbij1lem16  8392  fin23lem26  8482  fin23lem27  8485  fin1a2lem6  8562  itunitc  8578  axdc3lem2  8608  ttukeylem5  8670  fpwwe2lem13  8796  canthwelem  8804  pwfseqlem4  8816  wunex2  8892  wunex3  8895  inar1  8929  inatsk  8932  gruina  8972  suprzub  10933  uzsupss  10934  uzwo3  10935  rpnnen1lem4  10969  rpnnen1lem5  10970  supxrre  11277  infmxrre  11285  ioodisj  11401  supicclub2  11422  fzossnn0  11563  injresinjlem  11621  uzindi  11786  seqcoll  12199  seqcoll2  12200  limsupval2  12941  limsupgre  12942  limsupbnd2  12944  rlimuni  13011  rlimcld2  13039  rlimno1  13114  isercolllem2  13126  isercoll  13128  summolem2a  13175  summolem2  13176  fsumsers  13188  fsumcvg3  13189  4sqlem11  13998  vdwlem8  14031  vdwlem11  14034  ramub2  14057  0ram  14063  0ram2  14064  0ramcl  14066  ramub1lem2  14070  isohom  14692  funcres2c  14793  resscntz  15828  cntzidss  15834  cntzmhm2  15836  pgpssslw  16092  cntzspan  16305  gsumval3OLD  16361  gsumval3  16364  gsum2d  16436  gsum2dOLD  16437  dprdspan  16497  lssintcl  16966  lbsextlem2  17161  lbsextlem3  17162  lbsextlem4  17163  mplbas2  17482  mplbas2OLD  17483  islinds3  18104  fctop  18449  cctop  18451  neitr  18625  ordtbas2  18636  ordtopn1  18639  ordtopn2  18640  lmss  18743  clscon  18875  2ndcdisj  18901  2ndcomap  18903  ptbasfi  18995  txcmplem2  19056  hausdiag  19059  txkgen  19066  basqtop  19125  alexsubb  19459  alexsubALTlem4  19463  tsmsresOLD  19558  tsmsres  19559  tsmsxplem1  19568  tsmsxp  19570  ustrel  19627  utop3cls  19667  prdsmet  19786  metustrelOLD  19971  metustrel  19972  icccmplem2  20241  xrge0tsms  20252  cnmptre  20340  icchmeo  20354  bndth  20371  lebnumlem2  20375  cfilresi  20647  causs  20650  bcthlem5  20680  evthicc  20784  ovolficcss  20794  ovolmge0  20801  ovolgelb  20804  ovollb2lem  20812  ovollb2  20813  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliunlem2  20827  ovoliun  20829  ovolscalem1  20837  ovolicc1  20840  ovolicc2lem4  20844  ovolicc2  20846  voliunlem2  20873  voliunlem3  20874  ioombl1lem2  20881  ioombl1lem4  20883  uniioovol  20900  uniiccvol  20901  uniioombllem1  20902  uniioombllem2  20904  uniioombllem3  20906  uniioombllem4  20907  uniioombllem6  20909  dyadmbllem  20920  dyadmbl  20921  volcn  20927  vitalilem4  20932  vitalilem5  20933  cnmbf  20978  i1fmul  21015  itg1addlem4  21018  itg2seq  21061  dvbssntr  21216  dvreslem  21225  dvcjbr  21264  dvferm1  21298  dvferm2  21300  cmvth  21304  dvlip  21306  lhop1lem  21326  lhop2  21328  lhop  21329  dvcnvrelem2  21331  dvcnvre  21332  dvfsumle  21334  dvfsumge  21335  dvfsumabs  21336  dvfsumlem2  21340  ftc1a  21350  ftc1lem3  21351  ftc1lem6  21354  itgsubstlem  21361  mdegleb  21419  mdeglt  21420  mdegldg  21421  mdegxrcl  21422  mdegcl  21424  deg1mul3le  21472  ig1pdvds  21532  plyeq0lem  21562  aannenlem2  21679  aalioulem3  21684  taylf  21710  taylthlem2  21723  pserulm  21771  psercn2  21772  psercn  21775  reeff1olem  21795  efcvx  21798  loglesqr  22080  rlimcnp  22243  xrlimcnp  22246  jensen  22266  wilthlem2  22291  vmadivsumb  22616  pntrsumo1  22698  pntlem3  22742  axcontlem10  23041  usgraexmpl  23141  nmoxr  23988  nmooge0  23989  nmoolb  23993  nmoubi  23994  ubthlem1  24093  shmodi  24615  nmopxr  25092  nmfnxr  25105  nmoplb  25133  nmopub  25134  nmfnlb  25150  nmfnleub  25151  nmopun  25240  branmfn  25331  mdslj1i  25545  hatomistici  25588  suppss2f  25777  xppreima2  25788  fpwrelmap  25857  fzssnn  25896  xrge0tsmsd  26105  metideq  26173  metider  26174  pstmfval  26176  sigaclci  26428  insiga  26433  eulerpartlemgs2  26610  ballotlemsima  26745  signsply0  26799  rescon  26982  cvmliftlem8  27028  cvmlift3lem6  27060  prodmolem2a  27293  prodmolem2  27294  zprod  27296  nofulllem5  27693  heicant  28267  mblfinlem2  28270  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  itg2gt0cn  28288  ftc1cnnc  28307  ftc1anclem3  28310  ftc1anclem7  28314  ftc1anclem8  28315  ftc1anc  28316  areacirclem2  28326  areacirclem3  28327  areacirclem4  28328  ivthALT  28371  neibastop1  28421  topjoin  28427  totbndbnd  28529  prdsbnd  28533  heiborlem1  28551  rrnequiv  28575  reheibor  28579  iccbnd  28580  rmxyelqirr  29093  ttac  29227  hbtlem6  29327  hbt  29328  itgpowd  29432  ibliccsinexp  29634  iblioosinexp  29636  stoweidlem34  29672  stoweidlem59  29697  bnj1145  31683  bnj1137  31685  bnj1136  31687  pmapssbaN  32974  2polssN  33129  paddunN  33141  poldmj1N  33142  ispsubcl2N  33161  psubclinN  33162  paddatclN  33163  poml4N  33167  diaglbN  34270  diaintclN  34273  dibglbN  34381  dibintclN  34382  dicssdvh  34401  dihvalrel  34494  dochexmidlem4  34678
  Copyright terms: Public domain W3C validator