MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6ss Structured version   Visualization 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 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  difss2  3574  rintn0  4388  eqbrrdva  5026  ssxpb  5293  relfld  5384  funssxp  5769  dff2  6062  dff3  6063  fliftf  6238  1stcof  6853  2ndcof  6854  nnunifi  7853  elfiun  7975  marypha1lem  7978  marypha1  7979  ordtypelem7  8070  tcmin  8256  unwf  8312  rankfu  8379  tcrank  8386  aceq3lem  8582  dfac12lem2  8605  ackbij1lem9  8689  ackbij1lem10  8690  ackbij1lem16  8696  fin23lem26  8786  fin23lem27  8789  fin1a2lem6  8866  itunitc  8882  axdc3lem2  8912  ttukeylem5  8974  fpwwe2lem13  9098  canthwelem  9106  pwfseqlem4  9118  wunex2  9194  wunex3  9197  inar1  9231  inatsk  9234  gruina  9274  suprfinzcl  11084  suprzub  11289  uzsupss  11290  uzwo3  11293  rpnnen1lem4  11327  rpnnen1lem5  11328  supxrre  11647  infxrre  11656  infmxrreOLD  11660  ioodisj  11797  supicclub2  11818  fzssnn  11877  fzossnn0  11986  elfzom1elp1fzo  12018  injresinjlem  12062  uzindi  12232  ssnn0fi  12235  seqcoll  12666  seqcoll2  12667  reltrclfv  13136  relexpdmg  13160  relexpdm  13161  relexprng  13164  relexprn  13165  relexpfld  13167  relexpaddg  13171  limsupval2  13595  limsupval2OLD  13596  limsupgre  13597  limsupgreOLD  13598  limsupbnd2  13601  limsupbnd2OLD  13602  rlimuni  13669  rlimcld2  13697  rlimno1  13772  isercolllem2  13784  isercoll  13786  summolem2a  13836  summolem2  13837  fsumsers  13849  fsumcvg3  13850  prodmolem2a  14043  prodmolem2  14044  zprod  14046  lcmscllemOLD  14637  lcmfnnval  14649  lcmfnnvalOLD  14652  lcmfnncl  14657  4sqlem11  14954  vdwlem8  14993  vdwlem11  14996  ramub2  15026  0ram  15033  0ram2  15034  0ramcl  15036  ramub1lem2  15040  prmgaplem3  15078  prmgaplem4  15079  isohom  15736  funcres2c  15861  resscntz  17040  cntzidss  17046  cntzmhm2  17048  pgpssslw  17321  cntzspan  17537  gsumval3  17596  gsum2d  17659  dprdspan  17715  dprdres  17716  lssintcl  18242  lbsextlem2  18437  lbsextlem3  18438  lbsextlem4  18439  mplbas2  18749  islinds3  19447  fctop  20074  cctop  20076  neitr  20251  ordtbas2  20262  ordtopn1  20265  ordtopn2  20266  lmss  20369  clscon  20500  2ndcdisj  20526  2ndcomap  20528  ptbasfi  20651  txcmplem2  20712  hausdiag  20715  txkgen  20722  basqtop  20781  alexsubb  21116  alexsubALTlem4  21120  tsmsres  21213  tsmsxplem1  21222  tsmsxp  21224  ustrel  21281  utop3cls  21321  prdsmet  21440  metustrel  21622  icccmplem2  21896  xrge0tsms  21907  cnmptre  22010  icchmeo  22024  bndth  22041  lebnumlem2  22045  lebnumlem2OLD  22048  cfilresi  22320  causs  22323  bcthlem5  22351  evthicc  22465  ovolficcss  22477  ovolmge0  22485  ovolgelb  22488  ovollb2lem  22496  ovollb2  22497  ovolunlem1a  22504  ovolunlem1  22505  ovoliunlem1  22510  ovoliunlem2  22511  ovoliun  22513  ovolscalem1  22521  ovolicc1  22524  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  ovolicc2  22531  voliunlem2  22560  voliunlem3  22561  ioombl1lem2  22568  ioombl1lem4  22570  uniioovol  22592  uniiccvol  22593  uniioombllem1  22594  uniioombllem2  22596  uniioombllem2OLD  22597  uniioombllem3  22599  uniioombllem4  22600  uniioombllem6  22602  dyadmbllem  22613  dyadmbl  22614  volcn  22620  vitalilem4  22625  vitalilem5  22626  cnmbf  22671  i1fmul  22710  itg1addlem4  22713  itg2seq  22756  dvbssntr  22911  dvreslem  22920  dvcjbr  22959  dvferm1  22993  dvferm2  22995  cmvth  22999  dvlip  23001  lhop1lem  23021  lhop2  23023  lhop  23024  dvcnvrelem2  23026  dvcnvre  23027  dvfsumle  23029  dvfsumge  23030  dvfsumabs  23031  dvfsumlem2  23035  ftc1a  23045  ftc1lem3  23046  ftc1lem6  23049  itgsubstlem  23056  mdegleb  23069  mdeglt  23070  mdegldg  23071  mdegxrcl  23072  mdegcl  23074  deg1mul3le  23121  ig1pdvds  23184  ig1pdvdsOLD  23190  plyeq0lem  23220  aannenlem2  23341  aalioulem3  23346  taylf  23372  taylthlem2  23385  pserulm  23433  psercn2  23434  psercn  23437  reeff1olem  23457  efcvx  23460  loglesqrt  23754  rlimcnp  23947  xrlimcnp  23950  jensen  23970  wilthlem2  24050  vmadivsumb  24377  pntrsumo1  24459  pntlem3  24503  perpln2  24812  axcontlem10  25059  usgraexmplef  25184  nmoxr  26463  nmooge0  26464  nmoolb  26468  nmoubi  26469  ubthlem1  26568  shmodi  27099  nmopxr  27575  nmfnxr  27588  nmoplb  27616  nmopub  27617  nmfnlb  27633  nmfnleub  27634  nmopun  27723  branmfn  27814  mdslj1i  28028  hatomistici  28071  suppss2fOLD  28290  xppreima2  28302  fpwrelmap  28370  infxrge0gelb  28402  infxrge0gelbOLD  28403  xrge0tsmsd  28599  metideq  28747  metider  28748  pstmfval  28750  esumgect  28962  esum2d  28965  sigaclci  29005  insiga  29010  omssubadd  29178  omssubaddOLD  29182  eulerpartlemgs2  29263  ballotlemsima  29398  ballotlemsimaOLD  29436  signsply0  29490  bnj1145  29852  bnj1137  29854  bnj1136  29856  rescon  30019  cvmliftlem8  30065  cvmlift3lem6  30097  mclsssvlem  30250  mclsind  30258  mclsppslem  30271  nofulllem5  30645  ivthALT  31041  neibastop1  31065  topjoin  31071  ptrecube  31986  poimirlem6  31992  poimirlem15  32001  heicant  32021  mblfinlem2  32024  mblfinlem3  32025  mblfinlem4  32026  ismblfin  32027  itg2gt0cn  32043  ftc1cnnc  32062  ftc1anclem3  32065  ftc1anclem7  32069  ftc1anclem8  32070  ftc1anc  32071  areacirclem2  32079  areacirclem3  32080  areacirclem4  32081  totbndbnd  32167  prdsbnd  32171  heiborlem1  32189  rrnequiv  32213  reheibor  32217  iccbnd  32218  pmapssbaN  33371  2polssN  33526  paddunN  33538  poldmj1N  33539  ispsubcl2N  33558  psubclinN  33559  paddatclN  33560  poml4N  33564  diaglbN  34669  diaintclN  34672  dibglbN  34780  dibintclN  34781  dicssdvh  34800  dihvalrel  34893  dochexmidlem4  35077  rmxyelqirr  35804  ttac  35937  hbtlem6  36034  hbt  36035  itgpowd  36145  cnvssb  36238  cnvrcl0  36278  cnvtrrel  36308  relexpaddss  36356  cotrcltrcl  36363  cotrclrcl  36380  frege96d  36387  frege97d  36390  frege109d  36395  frege131d  36402  rp-imass  36412  uzfissfz  37624  suplesup  37637  limciccioolb  37787  limcicciooub  37803  limcleqr  37811  cncfiooicclem1  37857  ibliccsinexp  37913  iblioosinexp  37915  itgcoscmulx  37932  itgsincmulx  37937  itgsubsticclem  37938  itgiccshift  37943  itgperiod  37944  itgsbtaddcnst  37945  stoweidlem34  37996  stoweidlem59  38021  dirkeritg  38065  dirkercncflem2  38067  fourierdlem20  38090  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem39  38110  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem46  38117  fourierdlem52  38123  fourierdlem53  38124  fourierdlem60  38131  fourierdlem61  38132  fourierdlem62  38133  fourierdlem68  38139  fourierdlem76  38147  fourierdlem85  38156  fourierdlem88  38159  fourierdlem89  38160  fourierdlem90  38161  fourierdlem91  38162  fourierdlem93  38164  fourierdlem94  38165  fourierdlem103  38174  fourierdlem104  38175  fourierdlem111  38182  fouriersw  38196  etransclem46  38246  etransclem48OLD  38248  etransclem48  38249  sge0less  38337  sge0resplit  38351  sge0isum  38372  iccpartipre  38870  bgoldbtbndlem2  39036
  Copyright terms: Public domain W3C validator