Theorem syl5sseq 3489

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

Syntax hints:   -> wi 4   = wceq 1405   C_ wss 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3420  df-ss 3427

This theorem is referenced by:  fndmdif  5968  fneqeql2  5973  fconst4  6116  isofrlem  6218  f1opw2  6508  fparlem3  6885  fparlem4  6886  fnwelem  6898  frnsuppeq  6913  ecss  7389  pw2f1olem  7658  fopwdom  7662  ssenen  7728  phplem2  7734  ssfi  7774  fiint  7830  f1opwfi  7857  fisuppfi  7870  wemapso  8009  wemapso2OLD  8010  wemapso2lem  8011  cantnfcl  8117  cantnfle  8121  cantnflt  8122  cantnff  8124  cantnfp1lem2  8129  cantnfp1lem3  8130  cantnflem1b  8136  cantnflem1d  8138  cantnflem1  8139  cantnflem3  8141  cantnfclOLD  8147  cantnfleOLD  8151  cantnfltOLD  8152  cantnfp1lem2OLD  8155  cantnfp1lem3OLD  8156  cantnflem1bOLD  8159  cantnflem1dOLD  8161  cantnflem1OLD  8162  cantnflem3OLD  8163  cnfcomlem  8174  cnfcom  8175  cnfcom2lem  8176  cnfcom3lem  8178  cnfcom3  8179  cnfcomlemOLD  8182  cnfcomOLD  8183  cnfcom2lemOLD  8184  cnfcom3lemOLD  8186  cnfcom3OLD  8187  kmlem5  8565  enfin2i  8732  fin1a2lem7  8817  fpwwe2lem6  9042  fpwwe2lem9  9045  tskuni  9190  nn0suppOLD  10890  monoord2  12180  seqz  12197  isercolllem2  13635  isercolllem3  13636  fsumss  13694  binom1dif  13794  fprodss  13905  bpolycl  13995  bpolysum  13996  bpolydiflem  13997  bitsres  14330  vdwlem1  14706  vdwlem5  14710  vdwlem6  14711  prdshom  15079  imasless  15152  ghmpreima  16610  cntzval  16681  f1omvdmvd  16790  f1omvdconj  16793  pmtrfb  16812  pmtrfconj  16813  symggen  16817  symggen2  16818  psgnunilem1  16840  gsumval3OLD  17230  gsumval3lem1  17231  gsumval3lem2  17232  gsumval3  17233  gsumzres  17236  gsumzcl2  17237  gsumzf1o  17239  gsumzresOLD  17240  gsumzclOLD  17241  gsumzf1oOLD  17242  gsumzaddlem  17256  gsumzaddlemOLD  17258  gsumzmhm  17278  gsumzmhmOLD  17279  gsumzoppg  17288  gsumzoppgOLD  17289  gsum2d  17318  gsum2dOLD  17319  dpjidcl  17425  dpjidclOLD  17432  isdrngd  17739  lmhmpreima  18012  lspextmo  18020  mplcoe1  18445  mplcoe5  18449  mplcoe2OLD  18451  psr1baslem  18542  gsumfsum  18802  znleval  18889  regsumsupp  18954  frlmlbs  19122  mdetdiaglem  19390  ordtcld1  19989  ordtcld2  19990  cnpnei  20056  cnclima  20060  iscncl  20061  cnntri  20063  cnclsi  20064  cncls2  20065  cncls  20066  cnntr  20067  cncnp  20072  cndis  20083  paste  20086  cmpfi  20199  concompcld  20225  1stcfb  20236  1stccnp  20253  cldllycmp  20286  llycmpkgen2  20341  kgencn  20347  kgencn3  20349  dfac14lem  20408  txcnmpt  20415  txdis1cn  20426  hausdiag  20436  txkgen  20443  qtopval2  20487  basqtop  20502  qtopcld  20504  qtopcn  20505  qtopeu  20507  qtoprest  20508  imastopn  20511  hmeontr  20560  hmeoimaf1o  20561  cmphaushmeo  20591  ordthmeolem  20592  elfm3  20741  rnelfmlem  20743  rnelfm  20744  fmfnfmlem4  20748  alexsubALTlem4  20840  clssubg  20897  cldsubg  20899  tgpconcompeqg  20900  tgpconcomp  20901  tgphaus  20905  qustgpopn  20908  qustgplem  20909  tsmsgsum  20927  tsmsgsumOLD  20930  tsmsf1o  20937  ucncn  21078  xmeter  21226  imasf1oxms  21282  blcld  21298  metustssOLD  21346  metustss  21347  metustexhalfOLD  21356  metustexhalf  21357  metustfbasOLD  21358  metustfbas  21359  cfilucfilOLD  21362  cfilucfil  21363  metuel2  21372  restmetu  21380  icchmeo  21731  relcmpcmet  22045  rrxcph  22114  rrxsuppss  22120  minveclem4a  22135  nulmbl2  22237  icombl  22264  ioombl  22265  uniiccdif  22277  volivth  22306  mbfres2  22342  itg1addlem5  22397  itgsplitioo  22534  dvcobr  22639  dvcnvlem  22667  lhop1lem  22704  lhop  22707  dvcnvrelem2  22709  mdegfval  22750  mdegleb  22754  mdegldg  22756  deg1mul3le  22807  uc1pval  22830  mon1pval  22832  plyeq0lem  22897  dgrcl  22920  dgrub  22921  dgrlb  22923  vieta1lem1  22996  vieta1lem2  22997  basellem5  23737  f1otrg  24578  axlowdimlem13  24661  axcontlem10  24680  vdgrun  25305  vdgrfiun  25306  eupares  25379  eupath2lem3  25383  ssmd1  27629  mdslj2i  27638  atcvat4i  27715  iunxdif3  27843  imadifxp  27880  ofpreima  27936  ofpreima2  27937  qtophaus  28278  reff  28281  locfinreflem  28282  hauseqcn  28316  indpreima  28458  indf1ofs  28459  oms0  28731  sibfof  28774  eulerpartlemsv2  28789  eulerpartlemsf  28790  eulerpartlemv  28795  eulerpartlemb  28799  eulerpartlemt  28802  eulerpartlemr  28805  eulerpartlemgu  28808  eulerpartlemgs2  28811  eulerpartlemn  28812  ballotlemro  28953  bnj1253  29387  bnj1280  29390  subfacp1lem3  29466  cvmscld  29557  cvmsss2  29558  cvmliftmolem1  29565  cvmliftlem7  29575  cvmlift2lem9  29595  cvmlift3lem6  29608  cvmlift3lem7  29609  fnessref  30572  tailf  30590  mbfresfi  31413  cnambfre  31415  itg2addnclem  31419  itg2addnclem2  31420  mettrifi  31512  ismtyres  31566  isdrngo2  31623  keridl  31691  diaintclN  34058  dibintclN  34167  dihintcl  34344  dochocss  34366  mapdunirnN  34650  ismrcd1  34972  istopclsd  34974  pw2f1ocnv  35321  fsuppeq  35385  pwfi2f1o  35386  pwfi2f1oOLD  35387  itgcoscmulx  37117  ibliooicc  37119  stoweidlem11  37142  stoweidlem34  37165  fourierdlem48  37286  fourierdlem49  37287  fourierdlem74  37312  rngcbas  38265  ringcbas  38311  fdivmptf  38653  refdivmptf  38654