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

Theorem syl5sseq 3226
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 3200 . . 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 1623    C_ wss 3152
This theorem is referenced by:  fndmdif  5629  fneqeql2  5634  fconst4  5736  isofrlem  5837  f1opw2  6071  fparlem3  6220  fparlem4  6221  fnwelem  6230  ecss  6701  pw2f1olem  6966  fopwdom  6970  ssenen  7035  phplem2  7041  ssfi  7083  fiint  7133  f1opwfi  7159  wemapso  7266  wemapso2  7267  cantnfcl  7368  cantnfle  7372  cantnflt  7373  cantnff  7375  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cantnflem3  7393  cnfcomlem  7402  cnfcom  7403  cnfcom2lem  7404  cnfcom3lem  7406  cnfcom3  7407  kmlem5  7780  enfin2i  7947  fin1a2lem7  8032  fpwwe2lem6  8257  fpwwe2lem9  8260  tskuni  8405  nn0supp  10017  fzm1  10862  monoord2  11077  seqz  11094  isercolllem2  12139  isercolllem3  12140  fsumss  12198  binom1dif  12291  bitsres  12664  vdwlem1  13028  vdwlem5  13032  vdwlem6  13033  prdshom  13366  imasless  13442  fisuppfi  14450  ghmpreima  14704  cntzval  14797  gsumval3  15191  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumzmhm  15210  gsumzoppg  15216  gsum2d  15223  dpjidcl  15293  isdrngd  15537  lmhmpreima  15805  lspextmo  15813  mplcoe1  16209  mplcoe2  16211  psr1baslem  16264  gsumfsum  16439  znleval  16508  ordtcld1  16927  ordtcld2  16928  cnpnei  16993  cnclima  16997  iscncl  16998  cnntri  17000  cnclsi  17001  cncls2  17002  cncls  17003  cnntr  17004  cncnp  17009  cndis  17019  paste  17022  cmpfi  17135  concompcld  17160  1stcfb  17171  1stccnp  17188  cldllycmp  17221  llycmpkgen2  17245  kgencn  17251  kgencn3  17253  dfac14lem  17311  txcnmpt  17318  txdis1cn  17329  hausdiag  17339  txkgen  17346  qtopval2  17387  basqtop  17402  qtopcld  17404  qtopcn  17405  qtopeu  17407  qtoprest  17408  imastopn  17411  hmeontr  17460  hmeoimaf1o  17461  cmphaushmeo  17491  ordthmeolem  17492  elfm3  17645  rnelfmlem  17647  rnelfm  17648  fmfnfmlem4  17652  alexsubALTlem4  17744  clssubg  17791  cldsubg  17793  tgpconcompeqg  17794  tgpconcomp  17795  tgphaus  17799  divstgpopn  17802  divstgplem  17803  tsmsgsum  17821  tsmsf1o  17827  xmeter  17979  imasf1oxms  18035  blcld  18051  icchmeo  18439  relcmpcmet  18742  minveclem4a  18794  nulmbl2  18894  icombl  18921  ioombl  18922  uniiccdif  18933  volivth  18962  mbfres2  19000  itg1addlem5  19055  itgsplitioo  19192  dvcobr  19295  dvcnvlem  19323  lhop1lem  19360  lhop  19363  dvcnvrelem2  19365  mdegfval  19448  mdegleb  19450  mdegldg  19452  deg1mul3le  19502  uc1pval  19525  mon1pval  19527  plyeq0lem  19592  dgrcl  19615  dgrub  19616  dgrlb  19618  vieta1lem1  19690  vieta1lem2  19691  basellem5  20322  ssmd1  22891  mdslj2i  22900  atcvat4i  22977  ballotlemro  23081  indpreima  23608  indf1ofs  23609  subfacp1lem3  23713  cvmscld  23804  cvmsss2  23805  cvmliftmolem1  23812  cvmliftlem7  23822  cvmlift2lem9  23842  cvmlift3lem6  23855  cvmlift3lem7  23856  vdgrun  23893  eupares  23899  eupath2lem3  23903  axlowdimlem13  24582  axcontlem10  24601  bpolycl  24787  bpolysum  24788  bpolydiflem  24789  flfnei2  25577  islimrs4  25582  fnessref  26293  tailf  26324  mettrifi  26473  ismtyres  26532  isdrngo2  26589  keridl  26657  ismrcd1  26773  istopclsd  26775  pw2f1ocnv  27130  frlmlbs  27249  fsuppeq  27259  pwfi2f1o  27260  f1omvdmvd  27386  f1omvdconj  27389  pmtrfb  27406  pmtrfconj  27407  symggen  27411  symggen2  27412  psgnunilem1  27416  psgnghm2  27438  stoweidlem11  27760  stoweidlem34  27783  bnj1253  29047  bnj1280  29050  diaintclN  31248  dibintclN  31357  dihintcl  31534  dochocss  31556  mapdunirnN  31840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator