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

Theorem syl5sseq 3615
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseq.1 𝐵𝐴
syl5sseq.2 (𝜑𝐴 = 𝐶)
Assertion
Ref Expression
syl5sseq (𝜑𝐵𝐶)

Proof of Theorem syl5sseq
StepHypRef Expression
1 syl5sseq.2 . 2 (𝜑𝐴 = 𝐶)
2 syl5sseq.1 . 2 𝐵𝐴
3 sseq2 3589 . . 3 (𝐴 = 𝐶 → (𝐵𝐴𝐵𝐶))
43biimpa 499 . 2 ((𝐴 = 𝐶𝐵𝐴) → 𝐵𝐶)
51, 2, 4sylancl 692 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  iunxdif3  4536  fndmdif  6214  fneqeql2  6219  fconst4  6361  isofrlem  6468  f1opw2  6764  fparlem3  7144  fparlem4  7145  fnwelem  7157  frnsuppeq  7172  ecss  7653  pw2f1olem  7927  fopwdom  7931  ssenen  7997  phplem2  8003  ssfi  8043  fiint  8100  f1opwfi  8131  fisuppfi  8144  wemapso  8317  wemapso2lem  8318  cantnfcl  8425  cantnfle  8429  cantnflt  8430  cantnff  8432  cantnfp1lem2  8437  cantnfp1lem3  8438  cantnflem1b  8444  cantnflem1d  8446  cantnflem1  8447  cantnflem3  8449  cnfcomlem  8457  cnfcom  8458  cnfcom2lem  8459  cnfcom3lem  8461  cnfcom3  8462  kmlem5  8837  enfin2i  9004  fin1a2lem7  9089  fpwwe2lem6  9314  fpwwe2lem9  9317  tskuni  9462  monoord2  12652  seqz  12669  cshimadifsn0  13376  isercolllem2  14193  isercolllem3  14194  fsumss  14252  binom1dif  14353  fprodss  14466  bpolycl  14571  bpolysum  14572  bpolydiflem  14573  bitsres  14982  vdwlem1  15472  vdwlem5  15476  vdwlem6  15477  prdshom  15899  imasless  15972  ghmpreima  17454  cntzval  17526  f1omvdmvd  17635  f1omvdconj  17638  pmtrfb  17657  pmtrfconj  17658  symggen  17662  symggen2  17663  psgnunilem1  17685  gsumval3lem1  18078  gsumval3lem2  18079  gsumval3  18080  gsumzres  18082  gsumzcl2  18083  gsumzf1o  18085  gsumzaddlem  18093  gsumzmhm  18109  gsumzoppg  18116  gsum2d  18143  dpjidcl  18229  isdrngd  18544  lmhmpreima  18818  lspextmo  18826  mplcoe1  19235  mplcoe5  19238  psr1baslem  19325  gsumfsum  19581  znleval  19670  regsumsupp  19735  frlmlbs  19903  mdetdiaglem  20171  ordtcld1  20759  ordtcld2  20760  cnpnei  20826  cnclima  20830  iscncl  20831  cnntri  20833  cnclsi  20834  cncls2  20835  cncls  20836  cnntr  20837  cncnp  20842  cndis  20853  paste  20856  cmpfi  20969  concompcld  20995  1stcfb  21006  1stccnp  21023  cldllycmp  21056  llycmpkgen2  21111  kgencn  21117  kgencn3  21119  dfac14lem  21178  txcnmpt  21185  txdis1cn  21196  hausdiag  21206  txkgen  21213  qtopval2  21257  basqtop  21272  qtopcld  21274  qtopcn  21275  qtopeu  21277  qtoprest  21278  imastopn  21281  hmeontr  21330  hmeoimaf1o  21331  cmphaushmeo  21361  ordthmeolem  21362  elfm3  21512  rnelfmlem  21514  rnelfm  21515  fmfnfmlem4  21519  alexsubALTlem4  21612  clssubg  21670  cldsubg  21672  tgpconcompeqg  21673  tgpconcomp  21674  tgphaus  21678  qustgpopn  21681  qustgplem  21682  tsmsgsum  21700  tsmsf1o  21706  ucncn  21847  xmeter  21996  imasf1oxms  22052  blcld  22068  metustss  22114  metustexhalf  22119  metustfbas  22120  cfilucfil  22122  metuel2  22128  restmetu  22133  icchmeo  22496  relcmpcmet  22868  rrxcph  22933  rrxsuppss  22939  minveclem4a  22954  nulmbl2  23056  icombl  23084  ioombl  23085  uniiccdif  23097  volivth  23126  mbfres2  23163  itg1addlem5  23218  itgsplitioo  23355  dvcobr  23460  dvcnvlem  23488  lhop1lem  23525  lhop  23528  dvcnvrelem2  23530  mdegfval  23571  mdegleb  23573  mdegldg  23575  deg1mul3le  23625  uc1pval  23648  mon1pval  23650  plyeq0lem  23715  dgrcl  23738  dgrub  23739  dgrlb  23741  vieta1lem1  23814  vieta1lem2  23815  basellem5  24556  f1otrg  25497  axlowdimlem13  25580  axcontlem10  25599  vdgrun  26222  vdgrfiun  26223  eupares  26296  eupath2lem3  26300  ssmd1  28388  mdslj2i  28397  atcvat4i  28474  imadifxp  28630  ofpreima  28682  ofpreima2  28683  qtophaus  29065  reff  29068  locfinreflem  29069  hauseqcn  29103  indpreima  29248  indf1ofs  29249  oms0  29520  sibfof  29563  eulerpartlemsv2  29581  eulerpartlemsf  29582  eulerpartlemv  29587  eulerpartlemb  29591  eulerpartlemt  29594  eulerpartlemr  29597  eulerpartlemgu  29600  eulerpartlemgs2  29603  eulerpartlemn  29604  ballotlemro  29745  bnj1253  30173  bnj1280  30176  subfacp1lem3  30252  cvmscld  30343  cvmsss2  30344  cvmliftmolem1  30351  cvmliftlem7  30361  cvmlift2lem9  30381  cvmlift3lem6  30394  cvmlift3lem7  30395  fnessref  31356  tailf  31374  poimirlem3  32406  mbfresfi  32450  cnambfre  32452  itg2addnclem  32455  itg2addnclem2  32456  mettrifi  32547  ismtyres  32601  isdrngo2  32751  keridl  32825  diaintclN  35189  dibintclN  35298  dihintcl  35475  dochocss  35497  mapdunirnN  35781  ismrcd1  36103  istopclsd  36105  pw2f1ocnv  36446  pwfi2f1o  36508  wessf1ornlem  38190  itgcoscmulx  38685  ibliooicc  38687  stoweidlem11  38728  stoweidlem34  38751  fourierdlem48  38871  fourierdlem49  38872  fourierdlem74  38897  uhgrspansubgr  40537  vtxdun  40718  pthdlem1  40994  eucrct2eupth  41435  rngcbas  41779  ringcbas  41825  fdivmptf  42155  refdivmptf  42156
  Copyright terms: Public domain W3C validator