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

Theorem syl5sseq 3396
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 3370 . . 3  |-  ( A  =  C  ->  ( B  C_  A  <->  B  C_  C
) )
43biimpa 471 . 2  |-  ( ( A  =  C  /\  B  C_  A )  ->  B  C_  C )
51, 2, 4sylancl 644 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3320
This theorem is referenced by:  fndmdif  5834  fneqeql2  5839  fconst4  5956  isofrlem  6060  f1opw2  6298  fparlem3  6448  fparlem4  6449  fnwelem  6461  ecss  6946  pw2f1olem  7212  fopwdom  7216  ssenen  7281  phplem2  7287  ssfi  7329  fiint  7383  f1opwfi  7410  wemapso  7520  wemapso2  7521  cantnfcl  7622  cantnfle  7626  cantnflt  7627  cantnff  7629  cantnfp1lem2  7635  cantnfp1lem3  7636  cantnflem1b  7642  cantnflem1d  7644  cantnflem1  7645  cantnflem3  7647  cnfcomlem  7656  cnfcom  7657  cnfcom2lem  7658  cnfcom3lem  7660  cnfcom3  7661  kmlem5  8034  enfin2i  8201  fin1a2lem7  8286  fpwwe2lem6  8510  fpwwe2lem9  8513  tskuni  8658  nn0supp  10273  fzm1  11127  monoord2  11354  seqz  11371  isercolllem2  12459  isercolllem3  12460  fsumss  12519  binom1dif  12612  bitsres  12985  vdwlem1  13349  vdwlem5  13353  vdwlem6  13354  prdshom  13689  imasless  13765  fisuppfi  14773  ghmpreima  15027  cntzval  15120  gsumval3  15514  gsumzres  15517  gsumzcl  15518  gsumzf1o  15519  gsumzaddlem  15526  gsumzmhm  15533  gsumzoppg  15539  gsum2d  15546  dpjidcl  15616  isdrngd  15860  lmhmpreima  16124  lspextmo  16132  mplcoe1  16528  mplcoe2  16530  psr1baslem  16583  gsumfsum  16766  znleval  16835  ordtcld1  17261  ordtcld2  17262  cnpnei  17328  cnclima  17332  iscncl  17333  cnntri  17335  cnclsi  17336  cncls2  17337  cncls  17338  cnntr  17339  cncnp  17344  cndis  17355  paste  17358  cmpfi  17471  concompcld  17497  1stcfb  17508  1stccnp  17525  cldllycmp  17558  llycmpkgen2  17582  kgencn  17588  kgencn3  17590  dfac14lem  17649  txcnmpt  17656  txdis1cn  17667  hausdiag  17677  txkgen  17684  qtopval2  17728  basqtop  17743  qtopcld  17745  qtopcn  17746  qtopeu  17748  qtoprest  17749  imastopn  17752  hmeontr  17801  hmeoimaf1o  17802  cmphaushmeo  17832  ordthmeolem  17833  elfm3  17982  rnelfmlem  17984  rnelfm  17985  fmfnfmlem4  17989  alexsubALTlem4  18081  clssubg  18138  cldsubg  18140  tgpconcompeqg  18141  tgpconcomp  18142  tgphaus  18146  divstgpopn  18149  divstgplem  18150  tsmsgsum  18168  tsmsf1o  18174  ucncn  18315  xmeter  18463  imasf1oxms  18519  blcld  18535  metustssOLD  18583  metustss  18584  metustexhalfOLD  18593  metustexhalf  18594  metustfbasOLD  18595  metustfbas  18596  cfilucfilOLD  18599  cfilucfil  18600  metuel2  18609  restmetu  18617  icchmeo  18966  relcmpcmet  19269  minveclem4a  19331  nulmbl2  19431  icombl  19458  ioombl  19459  uniiccdif  19470  volivth  19499  mbfres2  19537  itg1addlem5  19592  itgsplitioo  19729  dvcobr  19832  dvcnvlem  19860  lhop1lem  19897  lhop  19900  dvcnvrelem2  19902  mdegfval  19985  mdegleb  19987  mdegldg  19989  deg1mul3le  20039  uc1pval  20062  mon1pval  20064  plyeq0lem  20129  dgrcl  20152  dgrub  20153  dgrlb  20155  vieta1lem1  20227  vieta1lem2  20228  basellem5  20867  vdgrun  21672  vdgrfiun  21673  eupares  21697  eupath2lem3  21701  ssmd1  23814  mdslj2i  23823  atcvat4i  23900  imadifxp  24038  ofpreima  24081  hauseqcn  24293  indpreima  24422  indf1ofs  24423  sibfof  24654  ballotlemro  24780  subfacp1lem3  24868  cvmscld  24960  cvmsss2  24961  cvmliftmolem1  24968  cvmliftlem7  24978  cvmlift2lem9  24998  cvmlift3lem6  25011  cvmlift3lem7  25012  fprodss  25274  axlowdimlem13  25893  axcontlem10  25912  bpolycl  26098  bpolysum  26099  bpolydiflem  26100  mbfresfi  26253  cnambfre  26255  itg2addnclem  26256  itg2addnclem2  26257  fnessref  26373  tailf  26404  mettrifi  26463  ismtyres  26517  isdrngo2  26574  keridl  26642  ismrcd1  26752  istopclsd  26754  pw2f1ocnv  27108  frlmlbs  27226  fsuppeq  27236  pwfi2f1o  27237  f1omvdmvd  27363  f1omvdconj  27366  pmtrfb  27383  pmtrfconj  27384  symggen  27388  symggen2  27389  psgnunilem1  27393  psgnghm2  27415  stoweidlem11  27736  stoweidlem34  27759  bnj1253  29386  bnj1280  29389  diaintclN  31856  dibintclN  31965  dihintcl  32142  dochocss  32164  mapdunirnN  32448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator