Theorem syl5sseq 3425

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 3399	. . 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 1369   C_ wss 3349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363

This theorem is referenced by:  fndmdif  5828  fneqeql2  5833  fconst4  5963  isofrlem  6052  f1opw2  6334  fparlem3  6695  fparlem4  6696  fnwelem  6708  frnsuppeq  6723  ecss  7163  pw2f1olem  7436  fopwdom  7440  ssenen  7506  phplem2  7512  ssfi  7554  fiint  7609  f1opwfi  7636  fisuppfi  7649  wemapso  7786  wemapso2OLD  7787  wemapso2lem  7788  cantnfcl  7896  cantnfle  7900  cantnflt  7901  cantnff  7903  cantnfp1lem2  7908  cantnfp1lem3  7909  cantnflem1b  7915  cantnflem1d  7917  cantnflem1  7918  cantnflem3  7920  cantnfclOLD  7926  cantnfleOLD  7930  cantnfltOLD  7931  cantnfp1lem2OLD  7934  cantnfp1lem3OLD  7935  cantnflem1bOLD  7938  cantnflem1dOLD  7940  cantnflem1OLD  7941  cantnflem3OLD  7942  cnfcomlem  7953  cnfcom  7954  cnfcom2lem  7955  cnfcom3lem  7957  cnfcom3  7958  cnfcomlemOLD  7961  cnfcomOLD  7962  cnfcom2lemOLD  7963  cnfcom3lemOLD  7965  cnfcom3OLD  7966  kmlem5  8344  enfin2i  8511  fin1a2lem7  8596  fpwwe2lem6  8823  fpwwe2lem9  8826  tskuni  8971  nn0suppOLD  10655  fzm1  11561  monoord2  11858  seqz  11875  isercolllem2  13164  isercolllem3  13165  fsumss  13223  binom1dif  13317  bitsres  13690  vdwlem1  14063  vdwlem5  14067  vdwlem6  14068  prdshom  14426  imasless  14499  ghmpreima  15789  cntzval  15860  f1omvdmvd  15970  f1omvdconj  15973  pmtrfb  15992  pmtrfconj  15993  symggen  15997  symggen2  15998  psgnunilem1  16020  gsumval3OLD  16403  gsumval3lem1  16404  gsumval3lem2  16405  gsumval3  16406  gsumzres  16409  gsumzcl2  16410  gsumzf1o  16412  gsumzresOLD  16413  gsumzclOLD  16414  gsumzf1oOLD  16415  gsumzaddlem  16429  gsumzaddlemOLD  16431  gsumzmhm  16452  gsumzmhmOLD  16453  gsumzoppg  16462  gsumzoppgOLD  16463  gsum2d  16485  gsum2dOLD  16486  dpjidcl  16579  dpjidclOLD  16586  isdrngd  16879  lmhmpreima  17151  lspextmo  17159  mplcoe1  17566  mplcoe5  17570  mplcoe2OLD  17572  psr1baslem  17663  gsumfsum  17901  znleval  18009  psgnghm2  18033  regsumsupp  18074  frlmlbs  18247  mdet1  18430  ordtcld1  18823  ordtcld2  18824  cnpnei  18890  cnclima  18894  iscncl  18895  cnntri  18897  cnclsi  18898  cncls2  18899  cncls  18900  cnntr  18901  cncnp  18906  cndis  18917  paste  18920  cmpfi  19033  concompcld  19060  1stcfb  19071  1stccnp  19088  cldllycmp  19121  llycmpkgen2  19145  kgencn  19151  kgencn3  19153  dfac14lem  19212  txcnmpt  19219  txdis1cn  19230  hausdiag  19240  txkgen  19247  qtopval2  19291  basqtop  19306  qtopcld  19308  qtopcn  19309  qtopeu  19311  qtoprest  19312  imastopn  19315  hmeontr  19364  hmeoimaf1o  19365  cmphaushmeo  19395  ordthmeolem  19396  elfm3  19545  rnelfmlem  19547  rnelfm  19548  fmfnfmlem4  19552  alexsubALTlem4  19644  clssubg  19701  cldsubg  19703  tgpconcompeqg  19704  tgpconcomp  19705  tgphaus  19709  divstgpopn  19712  divstgplem  19713  tsmsgsum  19731  tsmsgsumOLD  19734  tsmsf1o  19741  ucncn  19882  xmeter  20030  imasf1oxms  20086  blcld  20102  metustssOLD  20150  metustss  20151  metustexhalfOLD  20160  metustexhalf  20161  metustfbasOLD  20162  metustfbas  20163  cfilucfilOLD  20166  cfilucfil  20167  metuel2  20176  restmetu  20184  icchmeo  20535  relcmpcmet  20849  rrxcph  20918  rrxsuppss  20924  minveclem4a  20939  nulmbl2  21040  icombl  21067  ioombl  21068  uniiccdif  21080  volivth  21109  mbfres2  21145  itg1addlem5  21200  itgsplitioo  21337  dvcobr  21442  dvcnvlem  21470  lhop1lem  21507  lhop  21510  dvcnvrelem2  21512  mdegfval  21553  mdegleb  21557  mdegldg  21559  deg1mul3le  21610  uc1pval  21633  mon1pval  21635  plyeq0lem  21700  dgrcl  21723  dgrub  21724  dgrlb  21726  vieta1lem1  21798  vieta1lem2  21799  basellem5  22444  f1otrg  23139  axlowdimlem13  23222  axcontlem10  23241  vdgrun  23593  vdgrfiun  23594  eupares  23618  eupath2lem3  23622  ssmd1  25737  mdslj2i  25746  atcvat4i  25823  imadifxp  25961  ofpreima  26006  ofpreima2  26007  hauseqcn  26347  indpreima  26503  indf1ofs  26504  sibfof  26748  eulerpartlemsv2  26763  eulerpartlemsf  26764  eulerpartlemv  26769  eulerpartlemb  26773  eulerpartlemt  26776  eulerpartlemr  26779  eulerpartlemgu  26782  eulerpartlemgs2  26785  eulerpartlemn  26786  ballotlemro  26927  subfacp1lem3  27092  cvmscld  27184  cvmsss2  27185  cvmliftmolem1  27192  cvmliftlem7  27202  cvmlift2lem9  27222  cvmlift3lem6  27235  cvmlift3lem7  27236  fprodss  27483  bpolycl  28217  bpolysum  28218  bpolydiflem  28219  mbfresfi  28464  cnambfre  28466  itg2addnclem  28469  itg2addnclem2  28470  fnessref  28591  tailf  28622  mettrifi  28679  ismtyres  28733  isdrngo2  28790  keridl  28858  ismrcd1  29060  istopclsd  29062  pw2f1ocnv  29412  fsuppeq  29476  pwfi2f1o  29477  stoweidlem11  29832  stoweidlem34  29855  mdetdiaglem  30932  bnj1253  32104  bnj1280  32107  diaintclN  34799  dibintclN  34908  dihintcl  35085  dochocss  35107  mapdunirnN  35391