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

Theorem syl6ss 3456
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 3454 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-in 3423  df-ss 3430
This theorem is referenced by:  difss2  3574  rintn0  4367  eqbrrdva  4995  ssxpb  5261  relfld  5351  funssxp  5729  dff2  6023  dff3  6024  fliftf  6198  1stcof  6814  2ndcof  6815  nnunifi  7807  elfiun  7926  marypha1lem  7929  marypha1  7930  ordtypelem7  7985  tcmin  8206  unwf  8262  rankfu  8329  tcrank  8336  aceq3lem  8535  dfac12lem2  8558  ackbij1lem9  8642  ackbij1lem10  8643  ackbij1lem16  8649  fin23lem26  8739  fin23lem27  8742  fin1a2lem6  8819  itunitc  8835  axdc3lem2  8865  ttukeylem5  8927  fpwwe2lem13  9052  canthwelem  9060  pwfseqlem4  9072  wunex2  9148  wunex3  9151  inar1  9185  inatsk  9188  gruina  9228  suprfinzcl  11020  suprzub  11220  uzsupss  11221  uzwo3  11224  rpnnen1lem4  11258  rpnnen1lem5  11259  supxrre  11574  infmxrre  11582  ioodisj  11706  supicclub2  11727  fzossnn0  11890  elfzom1elp1fzo  11921  injresinjlem  11964  uzindi  12134  ssnn0fi  12137  seqcoll  12563  seqcoll2  12564  reltrclfv  13002  relexpdmg  13026  relexpdm  13027  relexprng  13030  relexprn  13031  relexpfld  13033  relexpaddg  13037  limsupval2  13454  limsupgre  13455  limsupbnd2  13457  rlimuni  13524  rlimcld2  13552  rlimno1  13627  isercolllem2  13639  isercoll  13641  summolem2a  13688  summolem2  13689  fsumsers  13701  fsumcvg3  13702  prodmolem2a  13895  prodmolem2  13896  zprod  13898  4sqlem11  14684  vdwlem8  14717  vdwlem11  14720  ramub2  14743  0ram  14749  0ram2  14750  0ramcl  14752  ramub1lem2  14756  isohom  15391  funcres2c  15516  resscntz  16695  cntzidss  16701  cntzmhm2  16703  pgpssslw  16960  cntzspan  17176  gsumval3OLD  17234  gsumval3  17237  gsum2d  17322  gsum2dOLD  17323  dprdspan  17396  dprdres  17397  lssintcl  17932  lbsextlem2  18127  lbsextlem3  18128  lbsextlem4  18129  mplbas2  18456  mplbas2OLD  18457  islinds3  19163  fctop  19799  cctop  19801  neitr  19976  ordtbas2  19987  ordtopn1  19990  ordtopn2  19991  lmss  20094  clscon  20225  2ndcdisj  20251  2ndcomap  20253  ptbasfi  20376  txcmplem2  20437  hausdiag  20440  txkgen  20447  basqtop  20506  alexsubb  20840  alexsubALTlem4  20844  tsmsresOLD  20939  tsmsres  20940  tsmsxplem1  20949  tsmsxp  20951  ustrel  21008  utop3cls  21048  prdsmet  21167  metustrelOLD  21352  metustrel  21353  icccmplem2  21622  xrge0tsms  21633  cnmptre  21721  icchmeo  21735  bndth  21752  lebnumlem2  21756  cfilresi  22028  causs  22031  bcthlem5  22061  evthicc  22165  ovolficcss  22175  ovolmge0  22182  ovolgelb  22185  ovollb2lem  22193  ovollb2  22194  ovolunlem1a  22201  ovolunlem1  22202  ovoliunlem1  22207  ovoliunlem2  22208  ovoliun  22210  ovolscalem1  22218  ovolicc1  22221  ovolicc2lem4  22225  ovolicc2  22227  voliunlem2  22255  voliunlem3  22256  ioombl1lem2  22263  ioombl1lem4  22265  uniioovol  22282  uniiccvol  22283  uniioombllem1  22284  uniioombllem2  22286  uniioombllem3  22288  uniioombllem4  22289  uniioombllem6  22291  dyadmbllem  22302  dyadmbl  22303  volcn  22309  vitalilem4  22314  vitalilem5  22315  cnmbf  22360  i1fmul  22397  itg1addlem4  22400  itg2seq  22443  dvbssntr  22598  dvreslem  22607  dvcjbr  22646  dvferm1  22680  dvferm2  22682  cmvth  22686  dvlip  22688  lhop1lem  22708  lhop2  22710  lhop  22711  dvcnvrelem2  22713  dvcnvre  22714  dvfsumle  22716  dvfsumge  22717  dvfsumabs  22718  dvfsumlem2  22722  ftc1a  22732  ftc1lem3  22733  ftc1lem6  22736  itgsubstlem  22743  mdegleb  22758  mdeglt  22759  mdegldg  22760  mdegxrcl  22761  mdegcl  22763  deg1mul3le  22811  ig1pdvds  22871  plyeq0lem  22901  aannenlem2  23019  aalioulem3  23024  taylf  23050  taylthlem2  23063  pserulm  23111  psercn2  23112  psercn  23115  reeff1olem  23135  efcvx  23138  loglesqrt  23430  rlimcnp  23623  xrlimcnp  23626  jensen  23646  wilthlem2  23726  vmadivsumb  24051  pntrsumo1  24133  pntlem3  24177  perpln2  24478  axcontlem10  24705  usgraexmpl  24830  nmoxr  26108  nmooge0  26109  nmoolb  26113  nmoubi  26114  ubthlem1  26213  shmodi  26735  nmopxr  27211  nmfnxr  27224  nmoplb  27252  nmopub  27253  nmfnlb  27269  nmfnleub  27270  nmopun  27359  branmfn  27450  mdslj1i  27664  hatomistici  27707  suppss2f  27933  xppreima2  27944  fpwrelmap  28016  infxrge0gelb  28041  fzssnn  28056  xrge0tsmsd  28241  metideq  28338  metider  28339  pstmfval  28341  esumgect  28550  esum2d  28553  sigaclci  28593  insiga  28598  omssubadd  28761  eulerpartlemgs2  28838  ballotlemsima  28973  signsply0  29027  bnj1145  29389  bnj1137  29391  bnj1136  29393  rescon  29556  cvmliftlem8  29602  cvmlift3lem6  29634  mclsssvlem  29787  mclsind  29795  mclsppslem  29808  nofulllem5  30179  ivthALT  30576  neibastop1  30600  topjoin  30606  heicant  31434  mblfinlem2  31437  mblfinlem3  31438  mblfinlem4  31439  ismblfin  31440  itg2gt0cn  31456  ftc1cnnc  31475  ftc1anclem3  31478  ftc1anclem7  31482  ftc1anclem8  31483  ftc1anc  31484  areacirclem2  31492  areacirclem3  31493  areacirclem4  31494  totbndbnd  31580  prdsbnd  31584  heiborlem1  31602  rrnequiv  31626  reheibor  31630  iccbnd  31631  pmapssbaN  32790  2polssN  32945  paddunN  32957  poldmj1N  32958  ispsubcl2N  32977  psubclinN  32978  paddatclN  32979  poml4N  32983  diaglbN  34088  diaintclN  34091  dibglbN  34199  dibintclN  34200  dicssdvh  34219  dihvalrel  34312  dochexmidlem4  34496  rmxyelqirr  35220  ttac  35353  hbtlem6  35455  hbt  35456  itgpowd  35559  cnvtrrel  35662  relexpaddss  35710  cotrcltrcl  35717  cotrclrcl  35734  frege96d  35741  frege97d  35744  frege109d  35749  frege131d  35756  rp-imass  35764  limciccioolb  37008  limcicciooub  37024  limcleqr  37031  cncfiooicclem1  37077  ibliccsinexp  37130  iblioosinexp  37132  itgcoscmulx  37149  itgsincmulx  37154  itgsubsticclem  37155  itgiccshift  37160  itgperiod  37161  itgsbtaddcnst  37162  stoweidlem34  37197  stoweidlem59  37222  dirkeritg  37265  dirkercncflem2  37267  fourierdlem20  37290  fourierdlem31  37301  fourierdlem39  37309  fourierdlem42  37312  fourierdlem46  37316  fourierdlem52  37322  fourierdlem53  37323  fourierdlem60  37330  fourierdlem61  37331  fourierdlem62  37332  fourierdlem68  37338  fourierdlem76  37346  fourierdlem85  37355  fourierdlem88  37358  fourierdlem89  37359  fourierdlem90  37360  fourierdlem91  37361  fourierdlem93  37363  fourierdlem94  37364  fourierdlem103  37373  fourierdlem104  37374  fourierdlem111  37381  fouriersw  37395  etransclem46  37444  etransclem48  37446  iccpartipre  37701  bgoldbtbndlem2  37867
  Copyright terms: Public domain W3C validator