Theorem syl5sseq 3537

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

Syntax hints:   -> wi 4   = wceq 1383   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  fndmdif  5976  fneqeql2  5981  fconst4  6121  isofrlem  6221  f1opw2  6513  fparlem3  6887  fparlem4  6888  fnwelem  6900  frnsuppeq  6915  ecss  7355  pw2f1olem  7623  fopwdom  7627  ssenen  7693  phplem2  7699  ssfi  7742  fiint  7799  f1opwfi  7826  fisuppfi  7839  wemapso  7979  wemapso2OLD  7980  wemapso2lem  7981  cantnfcl  8089  cantnfle  8093  cantnflt  8094  cantnff  8096  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1d  8110  cantnflem1  8111  cantnflem3  8113  cantnfclOLD  8119  cantnfleOLD  8123  cantnfltOLD  8124  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnflem3OLD  8135  cnfcomlem  8146  cnfcom  8147  cnfcom2lem  8148  cnfcom3lem  8150  cnfcom3  8151  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom2lemOLD  8156  cnfcom3lemOLD  8158  cnfcom3OLD  8159  kmlem5  8537  enfin2i  8704  fin1a2lem7  8789  fpwwe2lem6  9016  fpwwe2lem9  9019  tskuni  9164  nn0suppOLD  10857  fzm1  11768  monoord2  12119  seqz  12136  isercolllem2  13469  isercolllem3  13470  fsumss  13528  binom1dif  13626  fprodss  13736  bitsres  14104  vdwlem1  14480  vdwlem5  14484  vdwlem6  14485  prdshom  14845  imasless  14918  ghmpreima  16266  cntzval  16337  f1omvdmvd  16446  f1omvdconj  16449  pmtrfb  16468  pmtrfconj  16469  symggen  16473  symggen2  16474  psgnunilem1  16496  gsumval3OLD  16886  gsumval3lem1  16887  gsumval3lem2  16888  gsumval3  16889  gsumzres  16892  gsumzcl2  16893  gsumzf1o  16895  gsumzresOLD  16896  gsumzclOLD  16897  gsumzf1oOLD  16898  gsumzaddlem  16912  gsumzaddlemOLD  16914  gsumzmhm  16935  gsumzmhmOLD  16936  gsumzoppg  16945  gsumzoppgOLD  16946  gsum2d  16977  gsum2dOLD  16978  dpjidcl  17085  dpjidclOLD  17092  isdrngd  17399  lmhmpreima  17672  lspextmo  17680  mplcoe1  18105  mplcoe5  18109  mplcoe2OLD  18111  psr1baslem  18202  gsumfsum  18462  znleval  18570  regsumsupp  18635  frlmlbs  18808  mdetdiaglem  19077  ordtcld1  19675  ordtcld2  19676  cnpnei  19742  cnclima  19746  iscncl  19747  cnntri  19749  cnclsi  19750  cncls2  19751  cncls  19752  cnntr  19753  cncnp  19758  cndis  19769  paste  19772  cmpfi  19885  concompcld  19912  1stcfb  19923  1stccnp  19940  cldllycmp  19973  llycmpkgen2  20028  kgencn  20034  kgencn3  20036  dfac14lem  20095  txcnmpt  20102  txdis1cn  20113  hausdiag  20123  txkgen  20130  qtopval2  20174  basqtop  20189  qtopcld  20191  qtopcn  20192  qtopeu  20194  qtoprest  20195  imastopn  20198  hmeontr  20247  hmeoimaf1o  20248  cmphaushmeo  20278  ordthmeolem  20279  elfm3  20428  rnelfmlem  20430  rnelfm  20431  fmfnfmlem4  20435  alexsubALTlem4  20527  clssubg  20584  cldsubg  20586  tgpconcompeqg  20587  tgpconcomp  20588  tgphaus  20592  qustgpopn  20595  qustgplem  20596  tsmsgsum  20614  tsmsgsumOLD  20617  tsmsf1o  20624  ucncn  20765  xmeter  20913  imasf1oxms  20969  blcld  20985  metustssOLD  21033  metustss  21034  metustexhalfOLD  21043  metustexhalf  21044  metustfbasOLD  21045  metustfbas  21046  cfilucfilOLD  21049  cfilucfil  21050  metuel2  21059  restmetu  21067  icchmeo  21418  relcmpcmet  21732  rrxcph  21801  rrxsuppss  21807  minveclem4a  21822  nulmbl2  21924  icombl  21951  ioombl  21952  uniiccdif  21964  volivth  21993  mbfres2  22029  itg1addlem5  22084  itgsplitioo  22221  dvcobr  22326  dvcnvlem  22354  lhop1lem  22391  lhop  22394  dvcnvrelem2  22396  mdegfval  22437  mdegleb  22441  mdegldg  22443  deg1mul3le  22494  uc1pval  22517  mon1pval  22519  plyeq0lem  22584  dgrcl  22607  dgrub  22608  dgrlb  22610  vieta1lem1  22682  vieta1lem2  22683  basellem5  23334  f1otrg  24150  axlowdimlem13  24233  axcontlem10  24252  vdgrun  24877  vdgrfiun  24878  eupares  24951  eupath2lem3  24955  ssmd1  27206  mdslj2i  27215  atcvat4i  27292  imadifxp  27434  ofpreima  27483  ofpreima2  27484  qtophaus  27816  reff  27819  locfinreflem  27820  hauseqcn  27854  indpreima  28015  indf1ofs  28016  sibfof  28259  eulerpartlemsv2  28274  eulerpartlemsf  28275  eulerpartlemv  28280  eulerpartlemb  28284  eulerpartlemt  28287  eulerpartlemr  28290  eulerpartlemgu  28293  eulerpartlemgs2  28296  eulerpartlemn  28297  ballotlemro  28438  subfacp1lem3  28603  cvmscld  28695  cvmsss2  28696  cvmliftmolem1  28703  cvmliftlem7  28713  cvmlift2lem9  28733  cvmlift3lem6  28746  cvmlift3lem7  28747  bpolycl  29789  bpolysum  29790  bpolydiflem  29791  mbfresfi  30036  cnambfre  30038  itg2addnclem  30041  itg2addnclem2  30042  fnessref  30150  tailf  30168  mettrifi  30225  ismtyres  30279  isdrngo2  30336  keridl  30404  ismrcd1  30605  istopclsd  30607  pw2f1ocnv  30954  fsuppeq  31018  pwfi2f1o  31019  itgcoscmulx  31658  ibliooicc  31660  stoweidlem11  31682  stoweidlem34  31705  fourierdlem48  31826  fourierdlem49  31827  fourierdlem74  31852  rngcbas  32513  ringcbas  32556  bnj1253  33806  bnj1280  33809  diaintclN  36525  dibintclN  36634  dihintcl  36811  dochocss  36833  mapdunirnN  37117