Theorem syl5sseq 3492

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

Syntax hints:   -> wi 4   = wceq 1455   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430

This theorem is referenced by:  iunxdif3  4378  fndmdif  6014  fneqeql2  6019  fconst4  6159  isofrlem  6261  f1opw2  6554  fparlem3  6930  fparlem4  6931  fnwelem  6943  frnsuppeq  6958  ecss  7436  pw2f1olem  7707  fopwdom  7711  ssenen  7777  phplem2  7783  ssfi  7823  fiint  7879  f1opwfi  7909  fisuppfi  7922  wemapso  8097  wemapso2lem  8098  cantnfcl  8203  cantnfle  8207  cantnflt  8208  cantnff  8210  cantnfp1lem2  8215  cantnfp1lem3  8216  cantnflem1b  8222  cantnflem1d  8224  cantnflem1  8225  cantnflem3  8227  cnfcomlem  8235  cnfcom  8236  cnfcom2lem  8237  cnfcom3lem  8239  cnfcom3  8240  kmlem5  8615  enfin2i  8782  fin1a2lem7  8867  fpwwe2lem6  9091  fpwwe2lem9  9094  tskuni  9239  monoord2  12282  seqz  12299  isercolllem2  13784  isercolllem3  13785  fsumss  13846  binom1dif  13946  fprodss  14057  bpolycl  14160  bpolysum  14161  bpolydiflem  14162  bitsres  14502  vdwlem1  14986  vdwlem5  14990  vdwlem6  14991  prdshom  15420  imasless  15501  ghmpreima  16959  cntzval  17030  f1omvdmvd  17139  f1omvdconj  17142  pmtrfb  17161  pmtrfconj  17162  symggen  17166  symggen2  17167  psgnunilem1  17189  gsumval3lem1  17594  gsumval3lem2  17595  gsumval3  17596  gsumzres  17598  gsumzcl2  17599  gsumzf1o  17601  gsumzaddlem  17609  gsumzmhm  17625  gsumzoppg  17632  gsum2d  17659  dpjidcl  17746  isdrngd  18055  lmhmpreima  18326  lspextmo  18334  mplcoe1  18744  mplcoe5  18747  psr1baslem  18833  gsumfsum  19089  znleval  19180  regsumsupp  19245  frlmlbs  19410  mdetdiaglem  19678  ordtcld1  20268  ordtcld2  20269  cnpnei  20335  cnclima  20339  iscncl  20340  cnntri  20342  cnclsi  20343  cncls2  20344  cncls  20345  cnntr  20346  cncnp  20351  cndis  20362  paste  20365  cmpfi  20478  concompcld  20504  1stcfb  20515  1stccnp  20532  cldllycmp  20565  llycmpkgen2  20620  kgencn  20626  kgencn3  20628  dfac14lem  20687  txcnmpt  20694  txdis1cn  20705  hausdiag  20715  txkgen  20722  qtopval2  20766  basqtop  20781  qtopcld  20783  qtopcn  20784  qtopeu  20786  qtoprest  20787  imastopn  20790  hmeontr  20839  hmeoimaf1o  20840  cmphaushmeo  20870  ordthmeolem  20871  elfm3  21020  rnelfmlem  21022  rnelfm  21023  fmfnfmlem4  21027  alexsubALTlem4  21120  clssubg  21178  cldsubg  21180  tgpconcompeqg  21181  tgpconcomp  21182  tgphaus  21186  qustgpopn  21189  qustgplem  21190  tsmsgsum  21208  tsmsf1o  21214  ucncn  21355  xmeter  21503  imasf1oxms  21559  blcld  21575  metustss  21621  metustexhalf  21626  metustfbas  21627  cfilucfil  21629  metuel2  21635  restmetu  21640  icchmeo  22024  relcmpcmet  22341  rrxcph  22406  rrxsuppss  22412  minveclem4a  22427  minveclem4aOLD  22439  nulmbl2  22545  icombl  22573  ioombl  22574  uniiccdif  22591  volivth  22621  mbfres2  22657  itg1addlem5  22714  itgsplitioo  22851  dvcobr  22956  dvcnvlem  22984  lhop1lem  23021  lhop  23024  dvcnvrelem2  23026  mdegfval  23067  mdegleb  23069  mdegldg  23071  deg1mul3le  23121  uc1pval  23146  mon1pval  23148  plyeq0lem  23220  dgrcl  23243  dgrub  23244  dgrlb  23246  vieta1lem1  23319  vieta1lem2  23320  basellem5  24067  f1otrg  24957  axlowdimlem13  25040  axcontlem10  25059  vdgrun  25685  vdgrfiun  25686  eupares  25759  eupath2lem3  25763  ssmd1  28020  mdslj2i  28029  atcvat4i  28106  imadifxp  28265  ofpreima  28320  ofpreima2  28321  qtophaus  28714  reff  28717  locfinreflem  28718  hauseqcn  28752  indpreima  28897  indf1ofs  28898  oms0  29175  oms0OLD  29179  sibfof  29223  eulerpartlemsv2  29241  eulerpartlemsf  29242  eulerpartlemv  29247  eulerpartlemb  29251  eulerpartlemt  29254  eulerpartlemr  29257  eulerpartlemgu  29260  eulerpartlemgs2  29263  eulerpartlemn  29264  ballotlemro  29405  ballotlemroOLD  29443  bnj1253  29876  bnj1280  29879  subfacp1lem3  29955  cvmscld  30046  cvmsss2  30047  cvmliftmolem1  30054  cvmliftlem7  30064  cvmlift2lem9  30084  cvmlift3lem6  30097  cvmlift3lem7  30098  fnessref  31063  tailf  31081  poimirlem3  31989  mbfresfi  32033  cnambfre  32035  itg2addnclem  32039  itg2addnclem2  32040  mettrifi  32132  ismtyres  32186  isdrngo2  32243  keridl  32311  diaintclN  34672  dibintclN  34781  dihintcl  34958  dochocss  34980  mapdunirnN  35264  ismrcd1  35586  istopclsd  35588  pw2f1ocnv  35938  pwfi2f1o  36000  wessf1ornlem  37513  itgcoscmulx  37932  ibliooicc  37934  stoweidlem11  37972  stoweidlem34  37996  fourierdlem48  38119  fourierdlem49  38120  fourierdlem74  38145  uhgrspansubgr  39509  vtxduhgrun  39684  pthdlem1  39888  rngcbas  40336  ringcbas  40382  fdivmptf  40721  refdivmptf  40722