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

Theorem syl6ss 3501
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 3499 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  difss2  3618  rintn0  4406  eqbrrdva  5162  ssxpb  5431  relfld  5523  funssxp  5734  dff2  6028  dff3  6029  fliftf  6198  1stcof  6813  2ndcof  6814  nnunifi  7773  elfiun  7892  marypha1lem  7895  marypha1  7896  ordtypelem7  7952  tcmin  8175  unwf  8231  rankfu  8298  tcrank  8305  aceq3lem  8504  dfac12lem2  8527  ackbij1lem9  8611  ackbij1lem10  8612  ackbij1lem16  8618  fin23lem26  8708  fin23lem27  8711  fin1a2lem6  8788  itunitc  8804  axdc3lem2  8834  ttukeylem5  8896  fpwwe2lem13  9023  canthwelem  9031  pwfseqlem4  9043  wunex2  9119  wunex3  9122  inar1  9156  inatsk  9159  gruina  9199  suprfinzcl  10984  suprzub  11183  uzsupss  11184  uzwo3  11187  rpnnen1lem4  11221  rpnnen1lem5  11222  supxrre  11529  infmxrre  11537  ioodisj  11660  supicclub2  11681  fzossnn0  11837  elfzom1elp1fzo  11864  injresinjlem  11906  uzindi  12072  ssnn0fi  12075  seqcoll  12493  seqcoll2  12494  limsupval2  13284  limsupgre  13285  limsupbnd2  13287  rlimuni  13354  rlimcld2  13382  rlimno1  13457  isercolllem2  13469  isercoll  13471  summolem2a  13518  summolem2  13519  fsumsers  13531  fsumcvg3  13532  prodmolem2a  13722  prodmolem2  13723  zprod  13725  4sqlem11  14454  vdwlem8  14487  vdwlem11  14490  ramub2  14513  0ram  14519  0ram2  14520  0ramcl  14522  ramub1lem2  14526  isohom  15147  funcres2c  15248  resscntz  16347  cntzidss  16353  cntzmhm2  16355  pgpssslw  16612  cntzspan  16828  gsumval3OLD  16886  gsumval3  16889  gsum2d  16977  gsum2dOLD  16978  dprdspan  17052  dprdres  17053  lssintcl  17588  lbsextlem2  17783  lbsextlem3  17784  lbsextlem4  17785  mplbas2  18112  mplbas2OLD  18113  islinds3  18846  fctop  19482  cctop  19484  neitr  19658  ordtbas2  19669  ordtopn1  19672  ordtopn2  19673  lmss  19776  clscon  19908  2ndcdisj  19934  2ndcomap  19936  ptbasfi  20059  txcmplem2  20120  hausdiag  20123  txkgen  20130  basqtop  20189  alexsubb  20523  alexsubALTlem4  20527  tsmsresOLD  20622  tsmsres  20623  tsmsxplem1  20632  tsmsxp  20634  ustrel  20691  utop3cls  20731  prdsmet  20850  metustrelOLD  21035  metustrel  21036  icccmplem2  21305  xrge0tsms  21316  cnmptre  21404  icchmeo  21418  bndth  21435  lebnumlem2  21439  cfilresi  21711  causs  21714  bcthlem5  21744  evthicc  21848  ovolficcss  21858  ovolmge0  21865  ovolgelb  21868  ovollb2lem  21876  ovollb2  21877  ovolunlem1a  21884  ovolunlem1  21885  ovoliunlem1  21890  ovoliunlem2  21891  ovoliun  21893  ovolscalem1  21901  ovolicc1  21904  ovolicc2lem4  21908  ovolicc2  21910  voliunlem2  21938  voliunlem3  21939  ioombl1lem2  21946  ioombl1lem4  21948  uniioovol  21965  uniiccvol  21966  uniioombllem1  21967  uniioombllem2  21969  uniioombllem3  21971  uniioombllem4  21972  uniioombllem6  21974  dyadmbllem  21985  dyadmbl  21986  volcn  21992  vitalilem4  21997  vitalilem5  21998  cnmbf  22043  i1fmul  22080  itg1addlem4  22083  itg2seq  22126  dvbssntr  22281  dvreslem  22290  dvcjbr  22329  dvferm1  22363  dvferm2  22365  cmvth  22369  dvlip  22371  lhop1lem  22391  lhop2  22393  lhop  22394  dvcnvrelem2  22396  dvcnvre  22397  dvfsumle  22399  dvfsumge  22400  dvfsumabs  22401  dvfsumlem2  22405  ftc1a  22415  ftc1lem3  22416  ftc1lem6  22419  itgsubstlem  22426  mdegleb  22441  mdeglt  22442  mdegldg  22443  mdegxrcl  22444  mdegcl  22446  deg1mul3le  22494  ig1pdvds  22554  plyeq0lem  22584  aannenlem2  22701  aalioulem3  22706  taylf  22732  taylthlem2  22745  pserulm  22793  psercn2  22794  psercn  22797  reeff1olem  22817  efcvx  22820  loglesqrt  23108  rlimcnp  23271  xrlimcnp  23274  jensen  23294  wilthlem2  23319  vmadivsumb  23644  pntrsumo1  23726  pntlem3  23770  perpln2  24064  axcontlem10  24252  usgraexmpl  24377  nmoxr  25657  nmooge0  25658  nmoolb  25662  nmoubi  25663  ubthlem1  25762  shmodi  26284  nmopxr  26761  nmfnxr  26774  nmoplb  26802  nmopub  26803  nmfnlb  26819  nmfnleub  26820  nmopun  26909  branmfn  27000  mdslj1i  27214  hatomistici  27257  suppss2f  27453  xppreima2  27464  fpwrelmap  27532  fzssnn  27571  xrge0tsmsd  27752  metideq  27849  metider  27850  pstmfval  27852  sigaclci  28109  insiga  28114  eulerpartlemgs2  28296  ballotlemsima  28431  signsply0  28485  rescon  28668  cvmliftlem8  28714  cvmlift3lem6  28746  mclsssvlem  28899  mclsind  28907  mclsppslem  28920  nofulllem5  29441  heicant  30024  mblfinlem2  30027  mblfinlem3  30028  mblfinlem4  30029  ismblfin  30030  itg2gt0cn  30045  ftc1cnnc  30064  ftc1anclem3  30067  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  areacirclem2  30083  areacirclem3  30084  areacirclem4  30085  ivthALT  30128  neibastop1  30152  topjoin  30158  totbndbnd  30260  prdsbnd  30264  heiborlem1  30282  rrnequiv  30306  reheibor  30310  iccbnd  30311  rmxyelqirr  30821  ttac  30953  hbtlem6  31053  hbt  31054  itgpowd  31158  limciccioolb  31535  limcicciooub  31551  limcleqr  31558  cncfiooicclem1  31603  ibliccsinexp  31639  iblioosinexp  31641  itgcoscmulx  31658  itgsincmulx  31663  itgsubsticclem  31664  itgiccshift  31669  itgperiod  31670  itgsbtaddcnst  31671  stoweidlem34  31705  stoweidlem59  31730  dirkeritg  31773  dirkercncflem2  31775  fourierdlem20  31798  fourierdlem31  31809  fourierdlem39  31817  fourierdlem42  31820  fourierdlem46  31824  fourierdlem52  31830  fourierdlem53  31831  fourierdlem60  31838  fourierdlem61  31839  fourierdlem62  31840  fourierdlem68  31846  fourierdlem76  31854  fourierdlem85  31863  fourierdlem88  31866  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem93  31871  fourierdlem94  31872  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889  fouriersw  31903  bnj1145  33782  bnj1137  33784  bnj1136  33786  pmapssbaN  35224  2polssN  35379  paddunN  35391  poldmj1N  35392  ispsubcl2N  35411  psubclinN  35412  paddatclN  35413  poml4N  35417  diaglbN  36522  diaintclN  36525  dibglbN  36633  dibintclN  36634  dicssdvh  36653  dihvalrel  36746  dochexmidlem4  36930  cnvtrrel  37475  rp-imass  37482
  Copyright terms: Public domain W3C validator