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

Theorem syl5ss 3481
Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
Hypotheses
Ref Expression
syl5ss.1  |-  A  C_  B
syl5ss.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5ss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5ss
StepHypRef Expression
1 syl5ss.1 . . 3  |-  A  C_  B
21a1i 11 . 2  |-  ( ph  ->  A  C_  B )
3 syl5ss.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3sstrd 3480 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  wereu2  4851  sofld  5304  fvmptss  5974  fimacnv  6027  isofr2  6250  frxp  6917  fnse  6924  smores2  7081  f1imaen2g  7637  domunsncan  7678  fissuni  7885  fipreima  7886  dffi3  7951  marypha1lem  7953  ordtypelem7  8039  ordtypelem8  8040  oismo  8055  unxpwdom2  8103  cantnfres  8181  oemapvali  8188  tskwe  8383  acndom2  8483  dfac2a  8558  dfac12lem2  8572  cfle  8682  cofsmo  8697  coftr  8701  isf34lem5  8806  isf34lem7  8807  isf34lem6  8808  enfin1ai  8812  fin1a2lem12  8839  ttukeylem7  8943  alephexp1  9002  fpwwe2lem13  9066  fpwwe2  9067  canth4  9071  canthwelem  9074  pwfseqlem1  9082  pwfseqlem4  9086  fzossnn0  11947  fsuppmapnn0fiublem  12199  fsuppmapnn0fiub  12200  xptrrel  13023  limsupgle  13513  limsupgre  13520  limsupgreOLD  13521  rlimres  13600  lo1res  13601  lo1resb  13606  rlimresb  13607  o1resb  13608  o1of2  13654  o1rlimmul  13660  isercolllem2  13707  isercoll  13709  climsup  13711  fprodntriv  13974  bitsinvp1  14397  sadcaddlem  14405  sadadd2lem  14407  sadadd3  14409  sadasslem  14418  sadeq  14420  bitsres  14421  smuval2  14430  smupval  14436  smueqlem  14438  smumul  14441  1arith  14834  isstruct2  15093  setscom  15116  ressress  15149  imasvscafn  15394  imasless  15397  mrcssv  15471  isacs1i  15514  mreacs  15515  acsfn  15516  isacs4lem  16365  isacs5lem  16366  mhmima  16561  cntzmhm  16943  f1omvdconj  17038  f1omvdco2  17040  symgsssg  17059  symggen  17062  psgnunilem1  17085  efgval  17302  gsumzaddlem  17489  gsumconst  17502  dmdprdd  17566  dprdfeq0  17590  dprdres  17596  dprdss  17597  dprdz  17598  subgdmdprd  17602  dprddisj2  17607  dprd2dlem1  17609  dprd2da  17610  dprd2d2  17612  dmdprdsplit2lem  17613  lmhmlsp  18207  lsppratlem4  18308  islbs3  18313  lbsextlem3  18318  mplcoe5  18627  mplind  18660  znleval  19056  evpmss  19085  frlmsslsp  19285  lindff1  19309  lindfrn  19310  f1lindf  19311  lindfmm  19316  lsslindf  19319  basdif0  19899  tgcl  19916  ppttop  19953  epttop  19955  ntrin  20007  mretopd  20039  neiptoptop  20078  cnclsi  20219  cnconst2  20230  cnrest2  20233  cnpresti  20235  cnprest2  20237  fiuncmp  20350  connsub  20367  conima  20371  iunconlem  20373  1stcfb  20391  2ndc1stc  20397  2ndcdisj  20402  kgentopon  20484  llycmpkgen2  20496  1stckgenlem  20499  kgencn3  20504  ptclsg  20561  ptcnplem  20567  txtube  20586  hausdiag  20591  txkgen  20598  xkoco1cn  20603  xkoco2cn  20604  xkococnlem  20605  qtoptop2  20645  basqtop  20657  imastopn  20666  hmeores  20717  hmphdis  20742  ptcmpfi  20759  fbssfi  20783  filin  20800  infil  20809  fbasrn  20830  fgtr  20836  elfm  20893  imaelfm  20897  hausflim  20927  flimclslem  20930  fclscmp  20976  cnextcn  21013  tmdgsum2  21042  tgpconcomp  21058  ustexsym  21161  ustund  21167  ustimasn  21174  utoptop  21180  utopbas  21181  restutopopn  21184  blin2  21375  metustexhalf  21502  icccmplem2  21752  icccmplem3  21753  reconnlem2  21756  tchcph  22104  fmcfil  22135  resscdrg  22218  ivthlem2  22284  ivthlem3  22285  ivth2  22287  ovolfiniun  22332  ovoliunlem1  22333  ismbl2  22358  nulmbl2  22367  unmbl  22368  shftmbl  22369  voliunlem1  22380  voliunlem2  22381  ioombl1lem4  22391  uniioombllem4  22421  dyadmbllem  22434  dyadmbl  22435  mbflimsup  22500  mbflimsupOLD  22501  i1fima  22513  i1fima2  22514  i1fadd  22530  itg1addlem4  22534  itg2splitlem  22583  itg2split  22584  ellimc3  22711  limcflflem  22712  limcflf  22713  limcresi  22717  limciun  22726  dvreslem  22741  dvres2lem  22742  dvres  22743  dvaddbr  22769  dvmulbr  22770  dvlip  22822  dvlip2  22824  c1liplem1  22825  dvivthlem1  22837  dvne0  22840  lhop1lem  22842  lhop  22845  dvcnvrelem1  22846  dvcnvrelem2  22847  dvfsumle  22850  dvfsumabs  22852  dvfsumlem2  22856  itgsubstlem  22877  mdegleb  22890  mdeglt  22891  mdegldg  22892  mdegxrcl  22893  mdegcl  22895  ig1peu  22997  reeff1olem  23266  logccv  23473  rlimcnp2  23757  lgamgulmlem2  23820  ppisval  23893  prmdvdsfi  23897  mumul  23971  sqff1o  23972  chtlepsi  23997  chpub  24011  dchrisum0lem2a  24218  pntlem3  24310  ex-res  25736  ghsubgolemOLD  25943  htthlem  26405  chlejb1i  26964  ssmd2  27800  fimarab  28084  gsumle  28380  locfinreflem  28506  sibfof  29001  sitgclbn  29004  sitgaddlemb  29009  eulerpartlemgu  29036  ballotlemsima  29174  bnj1311  29621  erdsze2lem2  29715  iccllyscon  29761  cvmopnlem  29789  msrf  29968  nodenselem6  30360  nofulllem5  30380  neiin  30773  neibastop1  30800  neibastop2lem  30801  topmeet  30805  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem11  31655  poimirlem12  31656  poimirlem16  31660  poimirlem19  31663  poimirlem30  31674  cnambfre  31693  itg2gt0cn  31701  sstotbnd2  31810  sstotbnd3  31812  ssbnd  31824  ismtyima  31839  heibor1lem  31845  pmodlem2  33121  pmodN  33124  diaintclN  34335  djaclN  34413  dibintclN  34444  dicval  34453  dihoml4c  34653  djhcl  34677  isnacs2  35257  isnacs3  35261  diophrw  35310  pellfundre  35435  pellfundge  35436  pellfundlb  35438  pellfundglb  35439  fnwe2lem2  35615  lmhmfgima  35648  hbt  35695  trclrelexplem  35942  relexp0a  35947  rp-imass  36003  climinf  37256  climinfOLD  37257  islptre  37271  limccog  37272  limcleqr  37297  itgcoscmulx  37415  stoweidlem27  37456  dirkercncflem2  37535  fourierdlem38  37576  fourierdlem49  37587  fourierdlem51  37589  fourierdlem54  37592  fourierdlem63  37601  fourierdlem68  37606  fourierdlem69  37607  fourierdlem70  37608  fourierdlem74  37612  fourierdlem75  37613  fourierdlem76  37614  fourierdlem80  37618  fourierdlem84  37622  fourierdlem85  37623  fourierdlem88  37626  fourierdlem100  37638  fourierdlem101  37639  fourierdlem104  37642  fourierdlem107  37645  fourierdlem111  37649  fourierdlem112  37650  mgmhmima  38560
  Copyright terms: Public domain W3C validator