Theorem syl5ss 3614

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

Step	Hyp	Ref	Expression
1		syl5ss.1	. . 3 |- A C_ B
2	1	a1i 11	. 2 |- ( ph -> A C_ B )
3		syl5ss.2	. 2 |- ( ph -> B C_ C )
4	2, 3	sstrd 3613	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  wereu2  5111  sofld  5581  fvmptss  6292  fimacnv  6347  isofr2  6594  frxp  7287  fnse  7294  smores2  7451  f1imaen2g  8017  domunsncan  8060  dffi3  8337  marypha1lem  8339  ordtypelem7  8429  ordtypelem8  8430  oismo  8445  unxpwdom2  8493  cantnfres  8574  oemapvali  8581  tskwe  8776  acndom2  8877  dfac2a  8952  dfac12lem2  8966  cfle  9076  cofsmo  9091  coftr  9095  isf34lem5  9200  isf34lem7  9201  isf34lem6  9202  enfin1ai  9206  fin1a2lem12  9233  ttukeylem7  9337  alephexp1  9401  fpwwe2lem13  9464  fpwwe2  9465  canth4  9469  canthwelem  9472  pwfseqlem1  9480  pwfseqlem4  9484  fzossnn0  12499  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  xptrrel  13719  limsupgle  14208  limsupgre  14212  rlimres  14289  lo1res  14290  lo1resb  14295  rlimresb  14296  o1resb  14297  o1of2  14343  o1rlimmul  14349  isercolllem2  14396  isercoll  14398  climsup  14400  fprodntriv  14672  bitsinvp1  15171  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadasslem  15192  sadeq  15194  bitsres  15195  smuval2  15204  smupval  15210  smueqlem  15212  smumul  15215  1arith  15631  isstruct2  15867  setscom  15903  ressress  15938  imasvscafn  16197  imasless  16200  mrcssv  16274  isacs1i  16318  mreacs  16319  acsfn  16320  isacs4lem  17168  isacs5lem  17169  mhmima  17363  cntzmhm  17771  f1omvdconj  17866  f1omvdco2  17868  symgsssg  17887  symggen  17890  psgnunilem1  17913  efgval  18130  gsumzaddlem  18321  gsumconst  18334  dmdprdd  18398  dprdfeq0  18421  dprdres  18427  dprdss  18428  dprdz  18429  subgdmdprd  18433  dprddisj2  18438  dprd2dlem1  18440  dprd2da  18441  dprd2d2  18443  dmdprdsplit2lem  18444  lmhmlsp  19049  lsppratlem4  19150  islbs3  19155  lbsextlem3  19160  mplcoe5  19468  mplind  19502  znleval  19903  evpmss  19932  frlmsslsp  20135  lindff1  20159  lindfrn  20160  f1lindf  20161  lindfmm  20166  lsslindf  20169  basdif0  20757  tgcl  20773  ppttop  20811  epttop  20813  ntrin  20865  mretopd  20896  neiptoptop  20935  cnclsi  21076  cnconst2  21087  cnrest2  21090  cnpresti  21092  cnprest2  21094  fiuncmp  21207  connsub  21224  connima  21228  iunconnlem  21230  1stcfb  21248  2ndc1stc  21254  2ndcdisj  21259  kgentopon  21341  llycmpkgen2  21353  1stckgenlem  21356  kgencn3  21361  ptclsg  21418  ptcnplem  21424  txtube  21443  hausdiag  21448  txkgen  21455  xkoco1cn  21460  xkoco2cn  21461  xkococnlem  21462  qtoptop2  21502  basqtop  21514  imastopn  21523  hmeores  21574  hmphdis  21599  ptcmpfi  21616  fbssfi  21641  filin  21658  infil  21667  fbasrn  21688  fgtr  21694  elfm  21751  imaelfm  21755  hausflim  21785  flimclslem  21788  fclscmp  21834  cnextcn  21871  tmdgsum2  21900  tgpconncomp  21916  ustexsym  22019  ustund  22025  ustimasn  22032  utoptop  22038  utopbas  22039  restutopopn  22042  blin2  22234  metustexhalf  22361  icccmplem2  22626  icccmplem3  22627  reconnlem2  22630  tchcph  23036  fmcfil  23070  resscdrg  23154  ivthlem2  23221  ivthlem3  23222  ivth2  23224  ovolfiniun  23269  ovoliunlem1  23270  ismbl2  23295  nulmbl2  23304  unmbl  23305  shftmbl  23306  voliunlem1  23318  voliunlem2  23319  ioombl1lem4  23329  uniioombllem4  23354  dyadmbllem  23367  dyadmbl  23368  mbflimsup  23433  i1fima  23445  i1fima2  23446  i1fadd  23462  itg1addlem4  23466  itg2splitlem  23515  itg2split  23516  ellimc3  23643  limcflflem  23644  limcflf  23645  limcresi  23649  limciun  23658  dvreslem  23673  dvres2lem  23674  dvres  23675  dvaddbr  23701  dvmulbr  23702  dvlip  23756  dvlip2  23758  c1liplem1  23759  dvivthlem1  23771  dvne0  23774  lhop1lem  23776  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  itgsubstlem  23811  mdegleb  23824  mdeglt  23825  mdegldg  23826  mdegxrcl  23827  mdegcl  23829  ig1peu  23931  reeff1olem  24200  logccv  24409  rlimcnp2  24693  lgamgulmlem2  24756  ppisval  24830  prmdvdsfi  24833  mumul  24907  sqff1o  24908  chtlepsi  24931  chpub  24945  dchrisum0lem2a  25206  pntlem3  25298  ex-res  27298  htthlem  27774  chlejb1i  28335  ssmd2  29171  fimarab  29445  fz2ssnn0  29547  gsumle  29779  locfinreflem  29907  sibfof  30402  sitgclbn  30405  sitgaddlemb  30410  eulerpartlemgu  30439  ballotlemsima  30577  reprinrn  30696  bnj1311  31092  erdsze2lem2  31186  iccllysconn  31232  cvmopnlem  31260  msrf  31439  nosupno  31849  neiin  32327  neibastop1  32354  neibastop2lem  32355  topmeet  32359  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem19  33428  poimirlem30  33439  cnambfre  33458  itg2gt0cn  33465  sstotbnd2  33573  sstotbnd3  33575  ssbnd  33587  ismtyima  33602  heibor1lem  33608  idresssidinxp  34079  pmodlem2  35133  pmodN  35136  diaintclN  36347  djaclN  36425  dibintclN  36456  dicval  36465  dihoml4c  36665  djhcl  36689  isnacs2  37269  isnacs3  37273  diophrw  37322  pellfundre  37445  pellfundge  37446  pellfundlb  37448  pellfundglb  37449  fnwe2lem2  37621  lmhmfgima  37654  hbt  37700  cnvtrcl0  37933  trclrelexplem  38003  relexp0a  38008  rp-imass  38065  isotone2  38347  climinf  39838  islptre  39851  limccog  39852  limcleqr  39876  itgcoscmulx  40185  ismbl3  40203  ismbl4  40210  stoweidlem27  40244  dirkercncflem2  40321  fourierdlem38  40362  fourierdlem49  40372  fourierdlem51  40374  fourierdlem54  40377  fourierdlem63  40386  fourierdlem68  40391  fourierdlem69  40392  fourierdlem70  40393  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem80  40403  fourierdlem84  40407  fourierdlem85  40408  fourierdlem88  40411  fourierdlem100  40423  fourierdlem101  40424  fourierdlem104  40427  fourierdlem107  40430  fourierdlem111  40434  fourierdlem112  40435  caragenel2d  40746  hoidmv1lelem3  40807  hspmbllem3  40842  sssmf  40947  smfrec  40996  smfsuplem1  41017  mgmhmima  41802