Theorem syl5sseq 3552

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 3526	. . 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 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  fndmdif  5985  fneqeql2  5990  fconst4  6125  isofrlem  6224  f1opw2  6512  fparlem3  6885  fparlem4  6886  fnwelem  6898  frnsuppeq  6913  ecss  7353  pw2f1olem  7621  fopwdom  7625  ssenen  7691  phplem2  7697  ssfi  7740  fiint  7797  f1opwfi  7824  fisuppfi  7837  wemapso  7976  wemapso2OLD  7977  wemapso2lem  7978  cantnfcl  8086  cantnfle  8090  cantnflt  8091  cantnff  8093  cantnfp1lem2  8098  cantnfp1lem3  8099  cantnflem1b  8105  cantnflem1d  8107  cantnflem1  8108  cantnflem3  8110  cantnfclOLD  8116  cantnfleOLD  8120  cantnfltOLD  8121  cantnfp1lem2OLD  8124  cantnfp1lem3OLD  8125  cantnflem1bOLD  8128  cantnflem1dOLD  8130  cantnflem1OLD  8131  cantnflem3OLD  8132  cnfcomlem  8143  cnfcom  8144  cnfcom2lem  8145  cnfcom3lem  8147  cnfcom3  8148  cnfcomlemOLD  8151  cnfcomOLD  8152  cnfcom2lemOLD  8153  cnfcom3lemOLD  8155  cnfcom3OLD  8156  kmlem5  8534  enfin2i  8701  fin1a2lem7  8786  fpwwe2lem6  9013  fpwwe2lem9  9016  tskuni  9161  nn0suppOLD  10850  fzm1  11758  monoord2  12106  seqz  12123  isercolllem2  13451  isercolllem3  13452  fsumss  13510  binom1dif  13608  bitsres  13982  vdwlem1  14358  vdwlem5  14362  vdwlem6  14363  prdshom  14722  imasless  14795  ghmpreima  16093  cntzval  16164  f1omvdmvd  16274  f1omvdconj  16277  pmtrfb  16296  pmtrfconj  16297  symggen  16301  symggen2  16302  psgnunilem1  16324  gsumval3OLD  16711  gsumval3lem1  16712  gsumval3lem2  16713  gsumval3  16714  gsumzres  16717  gsumzcl2  16718  gsumzf1o  16720  gsumzresOLD  16721  gsumzclOLD  16722  gsumzf1oOLD  16723  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzmhm  16760  gsumzmhmOLD  16761  gsumzoppg  16770  gsumzoppgOLD  16771  gsum2d  16802  gsum2dOLD  16803  dpjidcl  16909  dpjidclOLD  16916  isdrngd  17221  lmhmpreima  17494  lspextmo  17502  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  psr1baslem  18023  gsumfsum  18280  znleval  18388  psgnghm2  18412  regsumsupp  18453  frlmlbs  18626  mdetdiaglem  18895  ordtcld1  19492  ordtcld2  19493  cnpnei  19559  cnclima  19563  iscncl  19564  cnntri  19566  cnclsi  19567  cncls2  19568  cncls  19569  cnntr  19570  cncnp  19575  cndis  19586  paste  19589  cmpfi  19702  concompcld  19729  1stcfb  19740  1stccnp  19757  cldllycmp  19790  llycmpkgen2  19814  kgencn  19820  kgencn3  19822  dfac14lem  19881  txcnmpt  19888  txdis1cn  19899  hausdiag  19909  txkgen  19916  qtopval2  19960  basqtop  19975  qtopcld  19977  qtopcn  19978  qtopeu  19980  qtoprest  19981  imastopn  19984  hmeontr  20033  hmeoimaf1o  20034  cmphaushmeo  20064  ordthmeolem  20065  elfm3  20214  rnelfmlem  20216  rnelfm  20217  fmfnfmlem4  20221  alexsubALTlem4  20313  clssubg  20370  cldsubg  20372  tgpconcompeqg  20373  tgpconcomp  20374  tgphaus  20378  divstgpopn  20381  divstgplem  20382  tsmsgsum  20400  tsmsgsumOLD  20403  tsmsf1o  20410  ucncn  20551  xmeter  20699  imasf1oxms  20755  blcld  20771  metustssOLD  20819  metustss  20820  metustexhalfOLD  20829  metustexhalf  20830  metustfbasOLD  20831  metustfbas  20832  cfilucfilOLD  20835  cfilucfil  20836  metuel2  20845  restmetu  20853  icchmeo  21204  relcmpcmet  21518  rrxcph  21587  rrxsuppss  21593  minveclem4a  21608  nulmbl2  21710  icombl  21737  ioombl  21738  uniiccdif  21750  volivth  21779  mbfres2  21815  itg1addlem5  21870  itgsplitioo  22007  dvcobr  22112  dvcnvlem  22140  lhop1lem  22177  lhop  22180  dvcnvrelem2  22182  mdegfval  22223  mdegleb  22227  mdegldg  22229  deg1mul3le  22280  uc1pval  22303  mon1pval  22305  plyeq0lem  22370  dgrcl  22393  dgrub  22394  dgrlb  22396  vieta1lem1  22468  vieta1lem2  22469  basellem5  23114  f1otrg  23878  axlowdimlem13  23961  axcontlem10  23980  vdgrun  24605  vdgrfiun  24606  eupares  24679  eupath2lem3  24683  ssmd1  26934  mdslj2i  26943  atcvat4i  27020  imadifxp  27159  ofpreima  27207  ofpreima2  27208  hauseqcn  27541  indpreima  27706  indf1ofs  27707  sibfof  27950  eulerpartlemsv2  27965  eulerpartlemsf  27966  eulerpartlemv  27971  eulerpartlemb  27975  eulerpartlemt  27978  eulerpartlemr  27981  eulerpartlemgu  27984  eulerpartlemgs2  27987  eulerpartlemn  27988  ballotlemro  28129  subfacp1lem3  28294  cvmscld  28386  cvmsss2  28387  cvmliftmolem1  28394  cvmliftlem7  28404  cvmlift2lem9  28424  cvmlift3lem6  28437  cvmlift3lem7  28438  fprodss  28685  bpolycl  29419  bpolysum  29420  bpolydiflem  29421  mbfresfi  29666  cnambfre  29668  itg2addnclem  29671  itg2addnclem2  29672  fnessref  29793  tailf  29824  mettrifi  29881  ismtyres  29935  isdrngo2  29992  keridl  30060  ismrcd1  30262  istopclsd  30264  pw2f1ocnv  30611  fsuppeq  30675  pwfi2f1o  30676  ibliooicc  31317  stoweidlem11  31339  stoweidlem34  31362  bnj1253  33170  bnj1280  33173  diaintclN  35873  dibintclN  35982  dihintcl  36159  dochocss  36181  mapdunirnN  36465