MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5sseq Unicode version

Theorem syl5sseq 3239
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
StepHypRef Expression
1 syl5sseq.2 . 2  |-  ( ph  ->  A  =  C )
2 syl5sseq.1 . 2  |-  B  C_  A
3 sseq2 3213 . . 3  |-  ( A  =  C  ->  ( B  C_  A  <->  B  C_  C
) )
43biimpa 470 . 2  |-  ( ( A  =  C  /\  B  C_  A )  ->  B  C_  C )
51, 2, 4sylancl 643 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  fndmdif  5645  fneqeql2  5650  fconst4  5752  isofrlem  5853  f1opw2  6087  fparlem3  6236  fparlem4  6237  fnwelem  6246  ecss  6717  pw2f1olem  6982  fopwdom  6986  ssenen  7051  phplem2  7057  ssfi  7099  fiint  7149  f1opwfi  7175  wemapso  7282  wemapso2  7283  cantnfcl  7384  cantnfle  7388  cantnflt  7389  cantnff  7391  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  cantnflem3  7409  cnfcomlem  7418  cnfcom  7419  cnfcom2lem  7420  cnfcom3lem  7422  cnfcom3  7423  kmlem5  7796  enfin2i  7963  fin1a2lem7  8048  fpwwe2lem6  8273  fpwwe2lem9  8276  tskuni  8421  nn0supp  10033  fzm1  10878  monoord2  11093  seqz  11110  isercolllem2  12155  isercolllem3  12156  fsumss  12214  binom1dif  12307  bitsres  12680  vdwlem1  13044  vdwlem5  13048  vdwlem6  13049  prdshom  13382  imasless  13458  fisuppfi  14466  ghmpreima  14720  cntzval  14813  gsumval3  15207  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumzmhm  15226  gsumzoppg  15232  gsum2d  15239  dpjidcl  15309  isdrngd  15553  lmhmpreima  15821  lspextmo  15829  mplcoe1  16225  mplcoe2  16227  psr1baslem  16280  gsumfsum  16455  znleval  16524  ordtcld1  16943  ordtcld2  16944  cnpnei  17009  cnclima  17013  iscncl  17014  cnntri  17016  cnclsi  17017  cncls2  17018  cncls  17019  cnntr  17020  cncnp  17025  cndis  17035  paste  17038  cmpfi  17151  concompcld  17176  1stcfb  17187  1stccnp  17204  cldllycmp  17237  llycmpkgen2  17261  kgencn  17267  kgencn3  17269  dfac14lem  17327  txcnmpt  17334  txdis1cn  17345  hausdiag  17355  txkgen  17362  qtopval2  17403  basqtop  17418  qtopcld  17420  qtopcn  17421  qtopeu  17423  qtoprest  17424  imastopn  17427  hmeontr  17476  hmeoimaf1o  17477  cmphaushmeo  17507  ordthmeolem  17508  elfm3  17661  rnelfmlem  17663  rnelfm  17664  fmfnfmlem4  17668  alexsubALTlem4  17760  clssubg  17807  cldsubg  17809  tgpconcompeqg  17810  tgpconcomp  17811  tgphaus  17815  divstgpopn  17818  divstgplem  17819  tsmsgsum  17837  tsmsf1o  17843  xmeter  17995  imasf1oxms  18051  blcld  18067  icchmeo  18455  relcmpcmet  18758  minveclem4a  18810  nulmbl2  18910  icombl  18937  ioombl  18938  uniiccdif  18949  volivth  18978  mbfres2  19016  itg1addlem5  19071  itgsplitioo  19208  dvcobr  19311  dvcnvlem  19339  lhop1lem  19376  lhop  19379  dvcnvrelem2  19381  mdegfval  19464  mdegleb  19466  mdegldg  19468  deg1mul3le  19518  uc1pval  19541  mon1pval  19543  plyeq0lem  19608  dgrcl  19631  dgrub  19632  dgrlb  19634  vieta1lem1  19706  vieta1lem2  19707  basellem5  20338  ssmd1  22907  mdslj2i  22916  atcvat4i  22993  ballotlemro  23097  indpreima  23623  indf1ofs  23624  subfacp1lem3  23728  cvmscld  23819  cvmsss2  23820  cvmliftmolem1  23827  cvmliftlem7  23837  cvmlift2lem9  23857  cvmlift3lem6  23870  cvmlift3lem7  23871  vdgrun  23908  eupares  23914  eupath2lem3  23918  axlowdimlem13  24654  axcontlem10  24673  bpolycl  24859  bpolysum  24860  bpolydiflem  24861  itg2addnclem  25003  itg2addnclem2  25004  flfnei2  25680  islimrs4  25685  fnessref  26396  tailf  26427  mettrifi  26576  ismtyres  26635  isdrngo2  26692  keridl  26760  ismrcd1  26876  istopclsd  26878  pw2f1ocnv  27233  frlmlbs  27352  fsuppeq  27362  pwfi2f1o  27363  f1omvdmvd  27489  f1omvdconj  27492  pmtrfb  27509  pmtrfconj  27510  symggen  27514  symggen2  27515  psgnunilem1  27519  psgnghm2  27541  stoweidlem11  27863  stoweidlem34  27886  bnj1253  29363  bnj1280  29366  diaintclN  31870  dibintclN  31979  dihintcl  32156  dochocss  32178  mapdunirnN  32462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator