Theorem syl5sseq 3356

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
syl5sseq.1	|- B C_ A
syl5sseq.2	|- ( ph -> A = C )

Assertion

Ref	Expression
syl5sseq	|- ( ph -> B C_ C )

Proof of Theorem syl5sseq

Step	Hyp	Ref	Expression
1		syl5sseq.2	. 2 |- ( ph -> A = C )
2		syl5sseq.1	. 2 |- B C_ A
3		sseq2 3330	. . 3 |- ( A = C -> ( B C_ A <-> B C_ C ) )
4	3	biimpa 471	. 2 |- ( ( A = C /\ B C_ A ) -> B C_ C )
5	1, 2, 4	sylancl 644	1 |- ( ph -> B C_ C )

Syntax hints:   -> wi 4   = wceq 1649   C_ wss 3280

This theorem is referenced by:  fndmdif  5793  fneqeql2  5798  fconst4  5915  isofrlem  6019  f1opw2  6257  fparlem3  6407  fparlem4  6408  fnwelem  6420  ecss  6905  pw2f1olem  7171  fopwdom  7175  ssenen  7240  phplem2  7246  ssfi  7288  fiint  7342  f1opwfi  7368  wemapso  7476  wemapso2  7477  cantnfcl  7578  cantnfle  7582  cantnflt  7583  cantnff  7585  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  cantnflem3  7603  cnfcomlem  7612  cnfcom  7613  cnfcom2lem  7614  cnfcom3lem  7616  cnfcom3  7617  kmlem5  7990  enfin2i  8157  fin1a2lem7  8242  fpwwe2lem6  8466  fpwwe2lem9  8469  tskuni  8614  nn0supp  10229  fzm1  11082  monoord2  11309  seqz  11326  isercolllem2  12414  isercolllem3  12415  fsumss  12474  binom1dif  12567  bitsres  12940  vdwlem1  13304  vdwlem5  13308  vdwlem6  13309  prdshom  13644  imasless  13720  fisuppfi  14728  ghmpreima  14982  cntzval  15075  gsumval3  15469  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumzmhm  15488  gsumzoppg  15494  gsum2d  15501  dpjidcl  15571  isdrngd  15815  lmhmpreima  16079  lspextmo  16087  mplcoe1  16483  mplcoe2  16485  psr1baslem  16538  gsumfsum  16721  znleval  16790  ordtcld1  17215  ordtcld2  17216  cnpnei  17282  cnclima  17286  iscncl  17287  cnntri  17289  cnclsi  17290  cncls2  17291  cncls  17292  cnntr  17293  cncnp  17298  cndis  17309  paste  17312  cmpfi  17425  concompcld  17450  1stcfb  17461  1stccnp  17478  cldllycmp  17511  llycmpkgen2  17535  kgencn  17541  kgencn3  17543  dfac14lem  17602  txcnmpt  17609  txdis1cn  17620  hausdiag  17630  txkgen  17637  qtopval2  17681  basqtop  17696  qtopcld  17698  qtopcn  17699  qtopeu  17701  qtoprest  17702  imastopn  17705  hmeontr  17754  hmeoimaf1o  17755  cmphaushmeo  17785  ordthmeolem  17786  elfm3  17935  rnelfmlem  17937  rnelfm  17938  fmfnfmlem4  17942  alexsubALTlem4  18034  clssubg  18091  cldsubg  18093  tgpconcompeqg  18094  tgpconcomp  18095  tgphaus  18099  divstgpopn  18102  divstgplem  18103  tsmsgsum  18121  tsmsf1o  18127  ucncn  18268  xmeter  18416  imasf1oxms  18472  blcld  18488  metustssOLD  18536  metustss  18537  metustexhalfOLD  18546  metustexhalf  18547  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  metuel2  18562  restmetu  18570  icchmeo  18919  relcmpcmet  19222  minveclem4a  19284  nulmbl2  19384  icombl  19411  ioombl  19412  uniiccdif  19423  volivth  19452  mbfres2  19490  itg1addlem5  19545  itgsplitioo  19682  dvcobr  19785  dvcnvlem  19813  lhop1lem  19850  lhop  19853  dvcnvrelem2  19855  mdegfval  19938  mdegleb  19940  mdegldg  19942  deg1mul3le  19992  uc1pval  20015  mon1pval  20017  plyeq0lem  20082  dgrcl  20105  dgrub  20106  dgrlb  20108  vieta1lem1  20180  vieta1lem2  20181  basellem5  20820  vdgrun  21625  vdgrfiun  21626  eupares  21650  eupath2lem3  21654  ssmd1  23767  mdslj2i  23776  atcvat4i  23853  imadifxp  23991  ofpreima  24034  hauseqcn  24246  indpreima  24375  indf1ofs  24376  sibfof  24607  ballotlemro  24733  subfacp1lem3  24821  cvmscld  24913  cvmsss2  24914  cvmliftmolem1  24921  cvmliftlem7  24931  cvmlift2lem9  24951  cvmlift3lem6  24964  cvmlift3lem7  24965  fprodss  25227  axlowdimlem13  25797  axcontlem10  25816  bpolycl  26002  bpolysum  26003  bpolydiflem  26004  mbfresfi  26152  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  fnessref  26263  tailf  26294  mettrifi  26353  ismtyres  26407  isdrngo2  26464  keridl  26532  ismrcd1  26642  istopclsd  26644  pw2f1ocnv  26998  frlmlbs  27117  fsuppeq  27127  pwfi2f1o  27128  f1omvdmvd  27254  f1omvdconj  27257  pmtrfb  27274  pmtrfconj  27275  symggen  27279  symggen2  27280  psgnunilem1  27284  psgnghm2  27306  stoweidlem11  27627  stoweidlem34  27650  bnj1253  29092  bnj1280  29095  diaintclN  31541  dibintclN  31650  dihintcl  31827  dochocss  31849  mapdunirnN  32133

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294