Theorem syl5sseq 3392

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 3366	. . 3 |- ( A = C -> ( B C_ A <-> B C_ C ) )
4	3	biimpa 481	. 2 |- ( ( A = C /\ B C_ A ) -> B C_ C )
5	1, 2, 4	sylancl 655	1 |- ( ph -> B C_ C )

Syntax hints:   -> wi 4   = wceq 1362   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330

This theorem is referenced by:  fndmdif  5795  fneqeql2  5800  fconst4  5929  isofrlem  6018  f1opw2  6302  fparlem3  6663  fparlem4  6664  fnwelem  6676  frnsuppeq  6691  ecss  7130  pw2f1olem  7403  fopwdom  7407  ssenen  7473  phplem2  7479  ssfi  7521  fiint  7576  f1opwfi  7603  fisuppfi  7616  wemapso  7753  wemapso2OLD  7754  wemapso2lem  7755  cantnfcl  7863  cantnfle  7867  cantnflt  7868  cantnff  7870  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1d  7884  cantnflem1  7885  cantnflem3  7887  cantnfclOLD  7893  cantnfleOLD  7897  cantnfltOLD  7898  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnflem3OLD  7909  cnfcomlem  7920  cnfcom  7921  cnfcom2lem  7922  cnfcom3lem  7924  cnfcom3  7925  cnfcomlemOLD  7928  cnfcomOLD  7929  cnfcom2lemOLD  7930  cnfcom3lemOLD  7932  cnfcom3OLD  7933  kmlem5  8311  enfin2i  8478  fin1a2lem7  8563  fpwwe2lem6  8789  fpwwe2lem9  8792  tskuni  8937  nn0suppOLD  10621  fzm1  11523  monoord2  11820  seqz  11837  isercolllem2  13126  isercolllem3  13127  fsumss  13185  binom1dif  13278  bitsres  13651  vdwlem1  14024  vdwlem5  14028  vdwlem6  14029  prdshom  14387  imasless  14460  ghmpreima  15747  cntzval  15818  f1omvdmvd  15928  f1omvdconj  15931  pmtrfb  15950  pmtrfconj  15951  symggen  15955  symggen2  15956  psgnunilem1  15978  gsumval3OLD  16361  gsumval3lem1  16362  gsumval3lem2  16363  gsumval3  16364  gsumzres  16367  gsumzcl2  16368  gsumzf1o  16370  gsumzresOLD  16371  gsumzclOLD  16372  gsumzf1oOLD  16373  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumzmhm  16406  gsumzmhmOLD  16407  gsumzoppg  16415  gsumzoppgOLD  16416  gsum2d  16436  gsum2dOLD  16437  dpjidcl  16530  dpjidclOLD  16537  isdrngd  16780  lmhmpreima  17050  lspextmo  17058  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  psr1baslem  17539  gsumfsum  17722  znleval  17828  psgnghm2  17852  regsumsupp  17893  frlmlbs  18066  mdet1  18249  ordtcld1  18642  ordtcld2  18643  cnpnei  18709  cnclima  18713  iscncl  18714  cnntri  18716  cnclsi  18717  cncls2  18718  cncls  18719  cnntr  18720  cncnp  18725  cndis  18736  paste  18739  cmpfi  18852  concompcld  18879  1stcfb  18890  1stccnp  18907  cldllycmp  18940  llycmpkgen2  18964  kgencn  18970  kgencn3  18972  dfac14lem  19031  txcnmpt  19038  txdis1cn  19049  hausdiag  19059  txkgen  19066  qtopval2  19110  basqtop  19125  qtopcld  19127  qtopcn  19128  qtopeu  19130  qtoprest  19131  imastopn  19134  hmeontr  19183  hmeoimaf1o  19184  cmphaushmeo  19214  ordthmeolem  19215  elfm3  19364  rnelfmlem  19366  rnelfm  19367  fmfnfmlem4  19371  alexsubALTlem4  19463  clssubg  19520  cldsubg  19522  tgpconcompeqg  19523  tgpconcomp  19524  tgphaus  19528  divstgpopn  19531  divstgplem  19532  tsmsgsum  19550  tsmsgsumOLD  19553  tsmsf1o  19560  ucncn  19701  xmeter  19849  imasf1oxms  19905  blcld  19921  metustssOLD  19969  metustss  19970  metustexhalfOLD  19979  metustexhalf  19980  metustfbasOLD  19981  metustfbas  19982  cfilucfilOLD  19985  cfilucfil  19986  metuel2  19995  restmetu  20003  icchmeo  20354  relcmpcmet  20668  rrxcph  20737  rrxsuppss  20743  minveclem4a  20758  nulmbl2  20859  icombl  20886  ioombl  20887  uniiccdif  20899  volivth  20928  mbfres2  20964  itg1addlem5  21019  itgsplitioo  21156  dvcobr  21261  dvcnvlem  21289  lhop1lem  21326  lhop  21329  dvcnvrelem2  21331  mdegfval  21415  mdegleb  21419  mdegldg  21421  deg1mul3le  21472  uc1pval  21495  mon1pval  21497  plyeq0lem  21562  dgrcl  21585  dgrub  21586  dgrlb  21588  vieta1lem1  21660  vieta1lem2  21661  basellem5  22306  f1otrg  22939  axlowdimlem13  23022  axcontlem10  23041  vdgrun  23393  vdgrfiun  23394  eupares  23418  eupath2lem3  23422  ssmd1  25537  mdslj2i  25546  atcvat4i  25623  imadifxp  25762  ofpreima  25807  ofpreima2  25808  nn0supp  25851  hauseqcn  26178  indpreima  26334  indf1ofs  26335  sibfof  26573  eulerpartlemsv2  26588  eulerpartlemsf  26589  eulerpartlemv  26594  eulerpartlemb  26598  eulerpartlemt  26601  eulerpartlemr  26604  eulerpartlemgu  26607  eulerpartlemgs2  26610  eulerpartlemn  26611  ballotlemro  26752  subfacp1lem3  26917  cvmscld  27009  cvmsss2  27010  cvmliftmolem1  27017  cvmliftlem7  27027  cvmlift2lem9  27047  cvmlift3lem6  27060  cvmlift3lem7  27061  fprodss  27307  bpolycl  28041  bpolysum  28042  bpolydiflem  28043  mbfresfi  28279  cnambfre  28281  itg2addnclem  28284  itg2addnclem2  28285  fnessref  28406  tailf  28437  mettrifi  28494  ismtyres  28548  isdrngo2  28605  keridl  28673  ismrcd1  28876  istopclsd  28878  pw2f1ocnv  29228  fsuppeq  29292  pwfi2f1o  29293  stoweidlem11  29649  stoweidlem34  29672  bnj1253  31707  bnj1280  31710  diaintclN  34273  dibintclN  34382  dihintcl  34559  dochocss  34581  mapdunirnN  34865