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

Theorem syl6sseqr 3801
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl6ssr.1 (𝜑𝐴𝐵)
syl6ssr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6sseqr (𝜑𝐴𝐶)

Proof of Theorem syl6sseqr
StepHypRef Expression
1 syl6ssr.1 . 2 (𝜑𝐴𝐵)
2 syl6ssr.2 . . 3 𝐶 = 𝐵
32eqcomi 2780 . 2 𝐵 = 𝐶
41, 3syl6sseq 3800 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737
This theorem is referenced by:  disjxiun  4783  knatar  6750  iunpw  7125  wfrdmcl  7576  wfrlem12  7579  wfrlem16  7583  wfrlem17  7584  tfrlem9  7634  tfrlem9a  7635  tfrlem13  7639  tz7.44-2  7656  tz7.44-3  7657  tz7.49  7693  marypha1lem  8495  ordtypelem2  8580  ixpiunwdom  8652  oemapvali  8745  tcss  8784  tcel  8785  pwwf  8834  rankpwi  8850  rankval3b  8853  cplem1  8916  dfac12lem2  9168  infmap2  9242  ackbij1b  9263  ttukeylem6  9538  fpwwe2lem11  9664  fpwwe2lem12  9665  fpwwe2lem13  9666  fpwwe2  9667  uznnssnn  11937  shftfval  14018  rexuzre  14300  climsup  14608  clim2prod  14827  fprodntriv  14879  eulerthlem2  15694  ramtlecl  15911  mreexexlem4d  16515  mreexdomd  16517  gsumpropd2lem  17481  gsumzaddlem  18528  gsum2d  18578  telgsums  18598  pgpfac1lem1  18681  pgpfac1lem3a  18683  pgpfac1lem3  18684  pgpfac1lem5  18686  lspsolvlem  19356  lbsextlem2  19374  dsmmacl  20302  eltopss  20932  difopn  21059  tgrest  21184  perfopn  21210  pnfnei  21245  mnfnei  21246  regsep2  21401  cncmp  21416  uncmp  21427  hauscmplem  21430  hauscmp  21431  conndisj  21440  cnconn  21446  conncompss  21457  2ndcctbss  21479  islly2  21508  comppfsc  21556  1stckgenlem  21577  txuni2  21589  ptbasfi  21605  ptpjopn  21636  txindis  21658  txtube  21664  hausdiag  21669  xkoinjcn  21711  tgqtop  21736  filconn  21907  elfm2  21972  flimclslem  22008  flffbas  22019  fclsbas  22045  flimfnfcls  22052  alexsubALT  22075  symgtgp  22125  ustssco  22238  isucn2  22303  ucnima  22305  ucnprima  22306  blcls  22531  prdsxmslem2  22554  isngp2  22621  tgioo  22819  xrtgioo  22829  xrsmopn  22835  opnreen  22854  cnheiborlem  22973  cnllycmp  22975  tchcph  23255  rrxmvallem  23406  uniioombllem4  23574  dyadmbllem  23587  opnmbllem  23589  mbfimaopnlem  23642  mbflimsup  23653  i1fadd  23682  i1fmul  23683  itg1addlem4  23686  i1fmulc  23690  limciun  23878  dvlip2  23978  c1lip3  23982  lhop  23999  dvfsumlem2  24010  dvfsumrlimge0  24013  dvfsumrlim2  24015  ulmval  24354  psercnlem2  24398  efopnlem2  24624  efopn  24625  umgrres1lem  26425  upgrres1  26428  nbgrssvwo2  26481  nbgrssvwo2OLD  26484  ubthlem1  28066  issh2  28406  mdsymlem1  29602  padct  29837  xrofsup  29873  fz2ssnn0  29887  tpr2rico  30298  sibfinima  30741  fct2relem  31015  bnj906  31338  bnj1014  31368  bnj1286  31425  bnj1408  31442  bnj1450  31456  bnj1452  31458  bnj1498  31467  bnj1501  31473  cvmopnlem  31598  cvmfolem  31599  cvmliftlem6  31610  cvmliftlem8  31612  cvmliftlem13  31616  cvmliftlem15  31618  cvmlift2lem9  31631  cvmlift2lem11  31633  cvmlift2lem12  31634  mclsppslem  31818  trpredpred  32064  trpredtr  32066  trpredrec  32074  frrlem5e  32125  frrlem11  32129  filnetlem4  32713  dissneqlem  33524  lindsdom  33736  opnmbllem0  33778  cnambfre  33790  heibor1lem  33940  osumcllem1N  35764  osumcllem2N  35765  pexmidlem6N  35783  dochexmidlem6  37275  dochexmidlem7  37276  mapdrvallem3  37456  k0004ss2  38976  dvsconst  39055  dvsid  39056  dvsef  39057  iunconnlem2  39693  uzssd2  40160  climinf  40356  climsuse  40358  climresmpt  40409  climleltrp  40426  stoweidlem28  40762  stoweidlem50  40784  stoweidlem52  40786  stoweidlem53  40787  stoweidlem54  40788  fourierdlem54  40894  fourierdlem80  40920  meaiininclem  41220  caratheodorylem2  41261  hspmbllem2  41361  mbfresmf  41468  smfmbfcex  41488  smflimlem2  41500  smflimsuplem2  41547  smflimsuplem3  41548  smflimsuplem5  41550  smflimsuplem6  41551  pfxccatpfx2  41956  upgredgssspr  42279  setrec1  42966  setrecsres  42976  aacllem  43078
  Copyright terms: Public domain W3C validator