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

Theorem syl5sseq 3686
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 3660 . . 3 (𝐴 = 𝐶 → (𝐵𝐴𝐵𝐶))
43biimpa 500 . 2 ((𝐴 = 𝐶𝐵𝐴) → 𝐵𝐶)
51, 2, 4sylancl 695 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  iunxdif3  4638  fndmdif  6361  fneqeql2  6366  fconst4  6519  isofrlem  6630  f1opw2  6930  fparlem3  7324  fparlem4  7325  fnwelem  7337  frnsuppeq  7352  ecss  7831  pw2f1olem  8105  fopwdom  8109  ssenen  8175  phplem2  8181  ssfi  8221  fiint  8278  f1opwfi  8311  fisuppfi  8324  wemapso  8497  wemapso2lem  8498  cantnfcl  8602  cantnfle  8606  cantnflt  8607  cantnff  8609  cantnfp1lem2  8614  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1d  8623  cantnflem1  8624  cantnflem3  8626  cnfcomlem  8634  cnfcom  8635  cnfcom2lem  8636  cnfcom3lem  8638  cnfcom3  8639  kmlem5  9014  enfin2i  9181  fin1a2lem7  9266  fpwwe2lem6  9495  fpwwe2lem9  9498  tskuni  9643  monoord2  12872  seqz  12889  cshimadifsn0  13622  isercolllem2  14440  isercolllem3  14441  fsumss  14500  binom1dif  14609  fprodss  14722  bpolycl  14827  bpolysum  14828  bpolydiflem  14829  bitsres  15242  vdwlem1  15732  vdwlem5  15736  vdwlem6  15737  prdshom  16174  imasless  16247  ghmpreima  17729  cntzval  17800  f1omvdmvd  17909  f1omvdconj  17912  pmtrfb  17931  pmtrfconj  17932  symggen  17936  symggen2  17937  psgnunilem1  17959  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumzmhm  18383  gsumzoppg  18390  gsum2d  18417  dpjidcl  18503  isdrngd  18820  lmhmpreima  19096  lspextmo  19104  mplcoe1  19513  mplcoe5  19516  psr1baslem  19603  gsumfsum  19861  znleval  19951  regsumsupp  20016  frlmlbs  20184  mdetdiaglem  20452  ordtcld1  21049  ordtcld2  21050  cnpnei  21116  cnclima  21120  iscncl  21121  cnntri  21123  cnclsi  21124  cncls2  21125  cncls  21126  cnntr  21127  cncnp  21132  cndis  21143  paste  21146  cmpfi  21259  conncompcld  21285  1stcfb  21296  1stccnp  21313  cldllycmp  21346  llycmpkgen2  21401  kgencn  21407  kgencn3  21409  dfac14lem  21468  txcnmpt  21475  txdis1cn  21486  hausdiag  21496  txkgen  21503  qtopval2  21547  basqtop  21562  qtopcld  21564  qtopcn  21565  qtopeu  21567  qtoprest  21568  imastopn  21571  hmeontr  21620  hmeoimaf1o  21621  cmphaushmeo  21651  ordthmeolem  21652  elfm3  21801  rnelfmlem  21803  rnelfm  21804  fmfnfmlem4  21808  alexsubALTlem4  21901  clssubg  21959  cldsubg  21961  tgpconncompeqg  21962  tgpconncomp  21963  tgphaus  21967  qustgpopn  21970  qustgplem  21971  tsmsgsum  21989  tsmsf1o  21995  ucncn  22136  xmeter  22285  imasf1oxms  22341  blcld  22357  metustss  22403  metustexhalf  22408  metustfbas  22409  cfilucfil  22411  metuel2  22417  restmetu  22422  icchmeo  22787  relcmpcmet  23161  rrxcph  23226  rrxsuppss  23232  minveclem4a  23247  nulmbl2  23350  icombl  23378  ioombl  23379  uniiccdif  23392  volivth  23421  mbfres2  23457  itg1addlem5  23512  itgsplitioo  23649  dvcobr  23754  dvcnvlem  23784  lhop1lem  23821  lhop  23824  dvcnvrelem2  23826  mdegfval  23867  mdegleb  23869  mdegldg  23871  deg1mul3le  23921  uc1pval  23944  mon1pval  23946  plyeq0lem  24011  dgrcl  24034  dgrub  24035  dgrlb  24037  vieta1lem1  24110  vieta1lem2  24111  basellem5  24856  f1otrg  25796  axlowdimlem13  25879  axcontlem10  25898  uhgrspansubgr  26228  vtxdun  26433  pthdlem1  26718  eucrct2eupth  27223  ssmd1  29298  mdslj2i  29307  atcvat4i  29384  imadifxp  29540  ofpreima  29593  ofpreima2  29594  qtophaus  30031  reff  30034  locfinreflem  30035  hauseqcn  30069  indpreima  30215  indf1ofs  30216  oms0  30487  sibfof  30530  eulerpartlemsv2  30548  eulerpartlemsf  30549  eulerpartlemv  30554  eulerpartlemb  30558  eulerpartlemt  30561  eulerpartlemr  30564  eulerpartlemgu  30567  eulerpartlemgs2  30570  eulerpartlemn  30571  ballotlemro  30712  bnj1253  31211  bnj1280  31214  subfacp1lem3  31290  cvmscld  31381  cvmsss2  31382  cvmliftmolem1  31389  cvmliftlem7  31399  cvmlift2lem9  31419  cvmlift3lem6  31432  cvmlift3lem7  31433  fnessref  32477  tailf  32495  poimirlem3  33542  mbfresfi  33586  cnambfre  33588  itg2addnclem  33591  itg2addnclem2  33592  mettrifi  33683  ismtyres  33737  isdrngo2  33887  keridl  33961  diaintclN  36664  dibintclN  36773  dihintcl  36950  dochocss  36972  mapdunirnN  37256  ismrcd1  37578  istopclsd  37580  pw2f1ocnv  37921  pwfi2f1o  37983  wessf1ornlem  39685  monoord2xrv  40027  itgcoscmulx  40503  ibliooicc  40505  stoweidlem11  40546  stoweidlem34  40569  fourierdlem48  40689  fourierdlem49  40690  fourierdlem74  40715  smfsuplem1  41338  rngcbas  42290  ringcbas  42336  fdivmptf  42660  refdivmptf  42661
  Copyright terms: Public domain W3C validator