Theorem syl5sseq 3653

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

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  iunxdif3  4606  fndmdif  6321  fneqeql2  6326  fconst4  6478  isofrlem  6590  f1opw2  6888  fparlem3  7279  fparlem4  7280  fnwelem  7292  frnsuppeq  7307  ecss  7788  pw2f1olem  8064  fopwdom  8068  ssenen  8134  phplem2  8140  ssfi  8180  fiint  8237  f1opwfi  8270  fisuppfi  8283  wemapso  8456  wemapso2lem  8457  cantnfcl  8564  cantnfle  8568  cantnflt  8569  cantnff  8571  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1d  8585  cantnflem1  8586  cantnflem3  8588  cnfcomlem  8596  cnfcom  8597  cnfcom2lem  8598  cnfcom3lem  8600  cnfcom3  8601  kmlem5  8976  enfin2i  9143  fin1a2lem7  9228  fpwwe2lem6  9457  fpwwe2lem9  9460  tskuni  9605  monoord2  12832  seqz  12849  cshimadifsn0  13576  isercolllem2  14396  isercolllem3  14397  fsumss  14456  binom1dif  14565  fprodss  14678  bpolycl  14783  bpolysum  14784  bpolydiflem  14785  bitsres  15195  vdwlem1  15685  vdwlem5  15689  vdwlem6  15690  prdshom  16127  imasless  16200  ghmpreima  17682  cntzval  17754  f1omvdmvd  17863  f1omvdconj  17866  pmtrfb  17885  pmtrfconj  17886  symggen  17890  symggen2  17891  psgnunilem1  17913  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumzmhm  18337  gsumzoppg  18344  gsum2d  18371  dpjidcl  18457  isdrngd  18772  lmhmpreima  19048  lspextmo  19056  mplcoe1  19465  mplcoe5  19468  psr1baslem  19555  gsumfsum  19813  znleval  19903  regsumsupp  19968  frlmlbs  20136  mdetdiaglem  20404  ordtcld1  21001  ordtcld2  21002  cnpnei  21068  cnclima  21072  iscncl  21073  cnntri  21075  cnclsi  21076  cncls2  21077  cncls  21078  cnntr  21079  cncnp  21084  cndis  21095  paste  21098  cmpfi  21211  conncompcld  21237  1stcfb  21248  1stccnp  21265  cldllycmp  21298  llycmpkgen2  21353  kgencn  21359  kgencn3  21361  dfac14lem  21420  txcnmpt  21427  txdis1cn  21438  hausdiag  21448  txkgen  21455  qtopval2  21499  basqtop  21514  qtopcld  21516  qtopcn  21517  qtopeu  21519  qtoprest  21520  imastopn  21523  hmeontr  21572  hmeoimaf1o  21573  cmphaushmeo  21603  ordthmeolem  21604  elfm3  21754  rnelfmlem  21756  rnelfm  21757  fmfnfmlem4  21761  alexsubALTlem4  21854  clssubg  21912  cldsubg  21914  tgpconncompeqg  21915  tgpconncomp  21916  tgphaus  21920  qustgpopn  21923  qustgplem  21924  tsmsgsum  21942  tsmsf1o  21948  ucncn  22089  xmeter  22238  imasf1oxms  22294  blcld  22310  metustss  22356  metustexhalf  22361  metustfbas  22362  cfilucfil  22364  metuel2  22370  restmetu  22375  icchmeo  22740  relcmpcmet  23115  rrxcph  23180  rrxsuppss  23186  minveclem4a  23201  nulmbl2  23304  icombl  23332  ioombl  23333  uniiccdif  23346  volivth  23375  mbfres2  23412  itg1addlem5  23467  itgsplitioo  23604  dvcobr  23709  dvcnvlem  23739  lhop1lem  23776  lhop  23779  dvcnvrelem2  23781  mdegfval  23822  mdegleb  23824  mdegldg  23826  deg1mul3le  23876  uc1pval  23899  mon1pval  23901  plyeq0lem  23966  dgrcl  23989  dgrub  23990  dgrlb  23992  vieta1lem1  24065  vieta1lem2  24066  basellem5  24811  f1otrg  25751  axlowdimlem13  25834  axcontlem10  25853  uhgrspansubgr  26183  vtxdun  26377  pthdlem1  26662  eucrct2eupth  27105  ssmd1  29170  mdslj2i  29179  atcvat4i  29256  imadifxp  29414  ofpreima  29465  ofpreima2  29466  qtophaus  29903  reff  29906  locfinreflem  29907  hauseqcn  29941  indpreima  30087  indf1ofs  30088  oms0  30359  sibfof  30402  eulerpartlemsv2  30420  eulerpartlemsf  30421  eulerpartlemv  30426  eulerpartlemb  30430  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemgu  30439  eulerpartlemgs2  30442  eulerpartlemn  30443  ballotlemro  30584  bnj1253  31085  bnj1280  31088  subfacp1lem3  31164  cvmscld  31255  cvmsss2  31256  cvmliftmolem1  31263  cvmliftlem7  31273  cvmlift2lem9  31293  cvmlift3lem6  31306  cvmlift3lem7  31307  fnessref  32352  tailf  32370  poimirlem3  33412  mbfresfi  33456  cnambfre  33458  itg2addnclem  33461  itg2addnclem2  33462  mettrifi  33553  ismtyres  33607  isdrngo2  33757  keridl  33831  opabssi  34130  diaintclN  36347  dibintclN  36456  dihintcl  36633  dochocss  36655  mapdunirnN  36939  ismrcd1  37261  istopclsd  37263  pw2f1ocnv  37604  pwfi2f1o  37666  wessf1ornlem  39371  itgcoscmulx  40185  ibliooicc  40187  stoweidlem11  40228  stoweidlem34  40251  fourierdlem48  40371  fourierdlem49  40372  fourierdlem74  40397  smfsuplem1  41017  rngcbas  41965  ringcbas  42011  fdivmptf  42335  refdivmptf  42336