Theorem syl5sseq 3509

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

Syntax hints:   -> wi 4   = wceq 1437   C_ wss 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447

This theorem is referenced by:  fndmdif  5993  fneqeql2  5998  fconst4  6136  isofrlem  6238  f1opw2  6528  fparlem3  6901  fparlem4  6902  fnwelem  6914  frnsuppeq  6929  ecss  7405  pw2f1olem  7674  fopwdom  7678  ssenen  7744  phplem2  7750  ssfi  7790  fiint  7846  f1opwfi  7876  fisuppfi  7889  wemapso  8064  wemapso2lem  8065  cantnfcl  8169  cantnfle  8173  cantnflt  8174  cantnff  8176  cantnfp1lem2  8181  cantnfp1lem3  8182  cantnflem1b  8188  cantnflem1d  8190  cantnflem1  8191  cantnflem3  8193  cnfcomlem  8201  cnfcom  8202  cnfcom2lem  8203  cnfcom3lem  8205  cnfcom3  8206  kmlem5  8580  enfin2i  8747  fin1a2lem7  8832  fpwwe2lem6  9056  fpwwe2lem9  9059  tskuni  9204  monoord2  12237  seqz  12254  isercolllem2  13707  isercolllem3  13708  fsumss  13769  binom1dif  13869  fprodss  13980  bpolycl  14083  bpolysum  14084  bpolydiflem  14085  bitsres  14425  vdwlem1  14909  vdwlem5  14913  vdwlem6  14914  prdshom  15343  imasless  15424  ghmpreima  16882  cntzval  16953  f1omvdmvd  17062  f1omvdconj  17065  pmtrfb  17084  pmtrfconj  17085  symggen  17089  symggen2  17090  psgnunilem1  17112  gsumval3lem1  17517  gsumval3lem2  17518  gsumval3  17519  gsumzres  17521  gsumzcl2  17522  gsumzf1o  17524  gsumzaddlem  17532  gsumzmhm  17548  gsumzoppg  17555  gsum2d  17582  dpjidcl  17669  isdrngd  17978  lmhmpreima  18249  lspextmo  18257  mplcoe1  18667  mplcoe5  18670  psr1baslem  18756  gsumfsum  19012  znleval  19102  regsumsupp  19167  frlmlbs  19332  mdetdiaglem  19600  ordtcld1  20190  ordtcld2  20191  cnpnei  20257  cnclima  20261  iscncl  20262  cnntri  20264  cnclsi  20265  cncls2  20266  cncls  20267  cnntr  20268  cncnp  20273  cndis  20284  paste  20287  cmpfi  20400  concompcld  20426  1stcfb  20437  1stccnp  20454  cldllycmp  20487  llycmpkgen2  20542  kgencn  20548  kgencn3  20550  dfac14lem  20609  txcnmpt  20616  txdis1cn  20627  hausdiag  20637  txkgen  20644  qtopval2  20688  basqtop  20703  qtopcld  20705  qtopcn  20706  qtopeu  20708  qtoprest  20709  imastopn  20712  hmeontr  20761  hmeoimaf1o  20762  cmphaushmeo  20792  ordthmeolem  20793  elfm3  20942  rnelfmlem  20944  rnelfm  20945  fmfnfmlem4  20949  alexsubALTlem4  21042  clssubg  21100  cldsubg  21102  tgpconcompeqg  21103  tgpconcomp  21104  tgphaus  21108  qustgpopn  21111  qustgplem  21112  tsmsgsum  21130  tsmsf1o  21136  ucncn  21277  xmeter  21425  imasf1oxms  21481  blcld  21497  metustss  21543  metustexhalf  21548  metustfbas  21549  cfilucfil  21551  metuel2  21557  restmetu  21562  icchmeo  21946  relcmpcmet  22263  rrxcph  22328  rrxsuppss  22334  minveclem4a  22349  minveclem4aOLD  22361  nulmbl2  22467  icombl  22494  ioombl  22495  uniiccdif  22512  volivth  22542  mbfres2  22578  itg1addlem5  22635  itgsplitioo  22772  dvcobr  22877  dvcnvlem  22905  lhop1lem  22942  lhop  22945  dvcnvrelem2  22947  mdegfval  22988  mdegleb  22990  mdegldg  22992  deg1mul3le  23042  uc1pval  23067  mon1pval  23069  plyeq0lem  23141  dgrcl  23164  dgrub  23165  dgrlb  23167  vieta1lem1  23240  vieta1lem2  23241  basellem5  23988  f1otrg  24878  axlowdimlem13  24961  axcontlem10  24980  vdgrun  25605  vdgrfiun  25606  eupares  25679  eupath2lem3  25683  ssmd1  27940  mdslj2i  27949  atcvat4i  28026  iunxdif3  28155  imadifxp  28192  ofpreima  28249  ofpreima2  28250  qtophaus  28652  reff  28655  locfinreflem  28656  hauseqcn  28690  indpreima  28835  indf1ofs  28836  oms0  29114  oms0OLD  29118  sibfof  29162  eulerpartlemsv2  29180  eulerpartlemsf  29181  eulerpartlemv  29186  eulerpartlemb  29190  eulerpartlemt  29193  eulerpartlemr  29196  eulerpartlemgu  29199  eulerpartlemgs2  29202  eulerpartlemn  29203  ballotlemro  29344  ballotlemroOLD  29382  bnj1253  29815  bnj1280  29818  subfacp1lem3  29894  cvmscld  29985  cvmsss2  29986  cvmliftmolem1  29993  cvmliftlem7  30003  cvmlift2lem9  30023  cvmlift3lem6  30036  cvmlift3lem7  30037  fnessref  30999  tailf  31017  poimirlem3  31851  mbfresfi  31895  cnambfre  31897  itg2addnclem  31901  itg2addnclem2  31902  mettrifi  31994  ismtyres  32048  isdrngo2  32105  keridl  32173  diaintclN  34539  dibintclN  34648  dihintcl  34825  dochocss  34847  mapdunirnN  35131  ismrcd1  35453  istopclsd  35455  pw2f1ocnv  35806  pwfi2f1o  35868  wessf1ornlem  37297  itgcoscmulx  37633  ibliooicc  37635  stoweidlem11  37658  stoweidlem34  37682  fourierdlem48  37805  fourierdlem49  37806  fourierdlem74  37831  rngcbas  39029  ringcbas  39075  fdivmptf  39417  refdivmptf  39418