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

Theorem syl6eqr 2333
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eqr.1  |-  ( ph  ->  A  =  B )
syl6eqr.2  |-  C  =  B
Assertion
Ref Expression
syl6eqr  |-  ( ph  ->  A  =  C )

Proof of Theorem syl6eqr
StepHypRef Expression
1 syl6eqr.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6eqr.2 . . 3  |-  C  =  B
32eqcomi 2287 . 2  |-  B  =  C
41, 3syl6eq 2331 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  3eqtr4g  2340  iinrab2  3965  relop  4834  dfiun3g  4931  dfiin3g  4932  resima2  4988  relcnvfld  5203  uniabio  5229  iotanul  5234  dffn5  5568  dfimafn2  5572  fncnvima2  5647  fmptcof  5692  fcoconst  5695  resfunexg  5737  ffnov  5948  fnov  5952  fnrnov  5993  foov  5994  funimassov  5997  ovelimab  5998  ofc12  6102  caofinvl  6104  1st2val  6145  2nd2val  6146  curry1  6210  curry2  6213  dftpos3  6252  riotav  6309  riotauni  6311  tz7.44-3  6421  rdgsucmptnf  6442  rdglim2a  6446  frsucmptn  6451  seqomlem1  6462  seqomlem4  6465  oa0r  6537  om1r  6541  oarec  6560  oacomf1olem  6562  oeeulem  6599  omabs  6645  ecinxp  6734  mapunen  7030  phplem1  7040  fodomfi  7135  iinfi  7171  fiin  7175  dffi3  7184  ordtypelem3  7235  ordtypelem9  7241  cantnffval  7364  cantnfval  7369  cantnfp1lem3  7382  cantnflem1  7391  wemapwe  7400  oef1o  7401  cnfcom2lem  7404  rankuni  7535  cardval2  7624  dfac8alem  7656  dfac12lem1  7769  cda1dif  7802  cdaassen  7808  isf34lem4  8003  hsmexlem5  8056  axdc3lem4  8079  axdc4lem  8081  ac6num  8106  zorn2lem1  8123  ttukeylem3  8138  pwcfsdom  8205  fpwwe2lem9  8260  canth4  8269  canthp1lem2  8275  genpass  8633  prlem934  8657  mulcmpblnrlem  8695  recexsrlem  8725  supsrlem  8733  axrnegex  8784  nneo  10095  cnref1o  10349  xmulneg1  10589  xmulpnf1n  10598  xadddi  10615  fztp  10841  fseq1m1p1  10858  uzrdgsuci  11023  mulexpz  11142  expaddz  11146  bcp1m1  11332  seqcoll  11401  iswrdi  11417  cjexp  11635  rexuz3  11832  limsupval  11948  limsupgle  11951  climconst  12017  zsum  12191  fsum  12193  sum0  12194  sumz  12195  fsumcnv  12236  incexc2  12297  mertenslem2  12341  efval2  12365  ege2le3  12371  efzval  12382  efival  12432  sinbnd  12460  cosbnd  12461  sadfval  12643  bitsres  12664  smufval  12668  smupp1  12671  eucalgval  12752  eucalginv  12754  eucalglt  12755  eucalgcvga  12756  eucalg  12757  dfphi2  12842  phimullem  12847  prmdiv  12853  odzval  12856  pcval  12897  pczpre  12900  pcrec  12911  prmreclem6  12968  4sqlem17  13008  vdwmc  13025  vdwpc  13027  vdwlem8  13035  ramval  13055  ramcl  13076  ressval  13195  resslem  13201  firest  13337  topnval  13339  prdsval  13355  prdsleval  13376  prdsbas3  13380  prdsdsval2  13383  pwsval  13385  pwsbas  13386  pwselbasb  13387  pwsplusgval  13389  pwsmulrval  13390  pwsle  13391  pwsvscafval  13393  imasval  13414  imasdsval  13418  imasdsval2  13419  divsval  13444  xpsval  13474  xpslem  13475  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  mrisval  13532  iscat  13574  cidfval  13578  homffval  13594  comfffval  13601  comffval  13602  comfeq  13609  oppcval  13616  oppchomfval  13617  oppccofval  13619  oppcbas  13621  oppcid  13624  monfval  13635  oppcmon  13641  sectffval  13653  invffval  13660  isoval  13667  isssc  13697  rescbas  13706  reschomf  13708  issubc  13712  isfunc  13738  isfuncd  13739  funcf2  13742  idfuval  13750  idfu2nd  13751  cofucl  13762  resfval2  13767  resf2nd  13769  funcres2b  13771  funcpropd  13774  isfull  13784  isfth  13788  natfval  13820  fucval  13832  fuccofval  13833  fucbas  13834  fuchom  13835  homafval  13861  homaval  13863  homadmcd  13874  arwval  13875  arwhoma  13877  idafval  13889  coafval  13896  coapm  13903  catcco  13933  catcid  13935  catcisolem  13938  xpcval  13951  xpcco  13957  1stfval  13965  2ndfval  13968  xpcpropd  13982  evlfval  13991  evlfcllem  13995  evlfcl  13996  curfval  13997  curf1cl  14002  curfcl  14006  uncf1  14010  uncf2  14011  uncfcurf  14013  diag2  14019  curf2ndf  14021  hofval  14026  hof2fval  14029  hofcl  14033  yonval  14035  hofpropd  14041  yonedalem21  14047  yonedalem22  14052  yonedalem3  14054  yonedainv  14055  yonffthlem  14056  isdrs  14068  ispos  14081  pltfval  14093  lubfval  14112  glbfval  14117  joinfval  14121  meetfval  14128  p0val  14147  p1val  14148  islat  14153  isclat  14215  ipoval  14257  isipodrs  14264  isdlat  14296  istsr  14326  spwval2  14333  isla  14342  isdir  14354  ismnd  14369  plusffval  14379  grpidval  14384  ismgmid  14387  pws0g  14408  ismhm  14417  submacs  14442  gsumvalx  14451  frmdval  14473  isgrp  14493  grpn0  14514  grpinvfval  14520  grpsubfval  14524  mulgfval  14568  mulgval  14569  mulgnn0p1  14578  pwsinvg  14607  issubg  14621  isnsg  14646  eqgfval  14665  divseccl  14673  isghm  14683  conjsubg  14714  conjsubgen  14715  isgim  14726  isga  14745  symgval  14771  cntrval  14795  cntzfval  14796  oppgval  14820  invoppggim  14833  odfval  14848  odval  14849  gexval  14889  ispgp  14903  sylow1lem1  14909  slwispgp  14922  pgpssslw  14925  sylow2alem2  14929  sylow3lem5  14942  lsmfval  14949  pj1fval  15003  efgmnvl  15023  efgval  15026  efgval2  15033  efginvrel2  15036  efgsfo  15048  efgredleme  15052  efgredlemd  15053  efgredlemc  15054  frgpval  15067  frgpeccl  15070  vrgpfval  15075  frgpuptinv  15080  frgpup3lem  15086  iscmn  15096  subcmn  15133  frgpnabllem1  15161  iscyg  15166  lt6abl  15181  gsumval3  15191  gsumzf1o  15196  gsum2d  15223  gsumcom2  15226  dmdprd  15236  dprdval  15238  dprd2da  15277  dmdprdsplit2lem  15280  dpjfval  15290  pgpfaclem1  15316  mgpval  15328  mgpplusg  15329  isrng  15345  iscrng  15348  pws1  15399  opprval  15406  crngoppr  15409  dvdsrval  15427  isunit  15439  invrfval  15455  dvrfval  15466  isirred  15481  dfrhm2  15498  pwsco1rhm  15510  pwsco2rhm  15511  isdrng  15516  isdrng2  15522  drngid  15526  isdrngrd  15538  issubrg  15545  abvfval  15583  abvneg  15599  staffval  15612  issrng  15615  issrngd  15626  islmod  15631  scaffval  15645  lssset  15691  prdsvscacl  15725  lspfval  15730  islmhm  15784  islmhm2  15795  islmim  15815  islbs  15829  islvec  15857  2idlval  15985  crng2idl  15991  isnzr  16011  rrgval  16028  isdomn  16035  isassa  16056  aspval  16068  asclfval  16074  psrval  16110  mvrfval  16165  mplval  16173  mplcoe3  16210  mplcoe2  16211  ltbval  16213  opsrval  16216  mplind  16243  vr1cl2  16272  ply1val  16273  psropprmul  16316  coe1mul2lem2  16345  coe1tm  16349  coe1sclmul  16358  coe1sclmul2  16360  ply1scl1  16367  ply1coe  16368  mulgrhm2  16461  zlmval  16470  chrval  16479  znval  16489  znzrhfo  16501  znle2  16507  znunithash  16518  cygznlem1  16520  isphl  16532  phllmhm  16536  ipffval  16552  ocvfval  16566  cssval  16582  cssincl  16588  thlval  16595  pjfval  16606  ishil  16618  isobs  16620  istps  16674  cldval  16760  ntrfval  16761  clsfval  16762  neifval  16836  lpfval  16870  isperf  16882  restbas  16889  tgrest  16890  resstopn  16916  ordtval  16919  ordtuni  16920  ordtbas  16922  ordtrest2  16934  ist0  17048  ist1  17049  ishaus  17050  iscnrm  17051  pnrmopn  17071  iscmp  17115  cmpcld  17129  hauscmplem  17133  cmpfi  17135  iscon  17139  consuba  17146  is1stc  17167  txval  17259  ptval  17265  ptbasin  17272  ptbasfi  17276  xkoval  17282  ptunimpt  17290  ptval2  17296  txbasval  17301  dfac14  17312  upxp  17317  uptx  17319  prdstopn  17322  txrest  17325  ptrescn  17333  lmcn2  17343  xkoptsub  17348  xkopt  17349  xkococn  17354  cnmpt2t  17367  cnmpt2res  17371  cnmpt2k  17382  qtopval  17386  imastopn  17411  hmphindis  17488  ptuncnv  17498  ptunhmeo  17499  xpstopnlem1  17500  xpstopnlem2  17502  xkohmeo  17506  qtophmeo  17508  elmptrab  17522  trfbas2  17538  trfil2  17582  fmco  17656  flimval  17658  flfcnp2  17702  fclsval  17703  fclsrest  17719  alexsublem  17738  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem1  17746  ptcmplem3  17748  ptcmpg  17751  istmd  17757  istgp  17760  istgp2  17774  tgplacthmeo  17786  clssubg  17791  tgpconcompeqg  17794  tsmsval2  17812  istrg  17846  istdrg  17848  istlm  17867  istvc  17874  imasdsf1olem  17937  xpsxmetlem  17943  xpsmet  17946  isxms  17993  isms  17995  tmsval  18027  stdbdxmet  18061  prdsxmslem2  18075  txmetcnp  18093  nmfval  18111  isngp  18118  tngval  18155  tngtopn  18166  tngnm  18167  isnrg  18171  isnlm  18186  nmofval  18223  nghmfval  18231  qtopbaslem  18267  cnblcld  18284  negcncf  18421  negfcncf  18422  cncfcnvcn  18424  cnmptre  18425  cnheiborlem  18452  cnheibor  18453  bndth  18456  pcorev2  18526  om1bas  18529  pi1val  18535  pi1bas3  18541  pi1cpbl  18542  pi1xfrcnv  18555  isclm  18562  nmoleub2lem3  18596  nmoleub3  18600  iscph  18606  cphcjcl  18619  tchval  18650  ipcau2  18664  csscld  18676  iscmet  18710  caubl  18733  caublcls  18734  bcthlem4  18749  bcthlem5  18750  bcth3  18753  isbn  18760  iscms  18767  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovolfsval  18830  ovolval  18833  ovollb2lem  18847  ovolctb  18849  ovolunlem1a  18855  ovoliunlem1  18861  ovoliun2  18865  shft2rab  18867  ovolshftlem1  18868  sca2rab  18871  ovolscalem1  18872  ovolicc2lem1  18876  ovolicc2lem4  18879  ovolicc2lem5  18880  cmmbl  18892  unmbl  18895  voliunlem3  18909  iunmbl  18910  voliun  18911  ioombl1lem3  18917  ovolfs2  18926  ioorinv  18931  uniiccdif  18933  uniioovol  18934  uniioombllem2a  18937  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombllem6  18943  dyadovol  18948  dyadss  18949  dyaddisjlem  18950  dyadmaxlem  18952  dyadmbl  18955  opnmbllem  18956  vitalilem4  18966  ismbf  18985  mbfconst  18990  itg2val  19083  itg2monolem1  19105  itg2i1fseq  19110  dfitg  19124  itgz  19135  itgvallem3  19140  iblcnlem1  19142  iblcnlem  19143  iblposlem  19146  itgreval  19151  itgfsum  19181  bddmulibl  19193  itgcn  19197  limcfval  19222  ellimc  19223  limcmpt2  19234  limccnp  19241  dvfval  19247  eldv  19248  dvreslem  19259  dvres2lem  19260  dvidlem  19265  dvnfval  19271  dvexp2  19303  dvrec  19304  dveflem  19326  dvlipcn  19341  dv11cn  19348  lhop  19363  ftc2  19391  evlsval  19403  evlsval2  19404  evlval  19408  evlrhm  19409  evl1fval  19410  evl1sca  19413  evl1var  19415  pf1subrg  19431  pf1ind  19438  mdegfval  19448  uc1pval  19525  mon1pval  19527  q1pval  19539  r1pval  19542  ig1pval  19558  plyconst  19588  plyeq0lem  19592  dgrval  19610  plyco  19623  0dgrb  19628  coemullem  19631  coe0  19637  coesub  19638  dgrsub  19653  dgrcolem1  19654  dgrcolem2  19655  dgrco  19656  quotval  19672  plydivex  19677  quotlem  19680  plyremlem  19684  fta1  19688  vieta1lem1  19690  vieta1lem2  19691  vieta1  19692  aaliou2  19720  aaliou3lem7  19729  taylpfval  19744  dvtaylp  19749  dvntaylp0  19751  taylthlem1  19752  ulm2  19764  ulmshft  19769  pserdvlem2  19804  abelthlem1  19807  abelthlem8  19815  abelth  19817  abelth2  19818  ptolemy  19864  coskpi  19888  efif1olem2  19905  efif1olem3  19906  logcnlem4  19992  advlogexp  20002  efopn  20005  logtayl  20007  dcubic2  20140  dcubic  20142  quart1lem  20151  atancj  20206  tanatan  20215  cosatan  20217  dvatan  20231  leibpi  20238  birthdaylem2  20247  efrlim  20264  emcllem7  20295  wilthlem2  20307  basellem5  20322  basellem8  20325  basellem9  20326  vmaval  20351  prmorcht  20416  mumul  20419  dvdsmulf1o  20434  fsumdvdsmul  20435  ppiub  20443  fsumvma  20452  pclogsum  20454  dchrval  20473  bposlem8  20530  lgslem1  20535  lgsval  20539  lgsval4  20555  lgsfcl3  20556  lgsdilem  20561  lgsdir2lem4  20565  lgsdir2lem5  20566  lgsquadlem2  20594  dchrisum0flb  20659  rpvmasum2  20661  log2sumbnd  20693  selberglem2  20695  pntibndlem2  20740  pntlemp  20759  ostth2lem3  20784  ostth2lem4  20785  isplig  20844  gidval  20880  grpoinvfval  20891  grpodivfval  20909  gxfval  20924  isablo  20950  subgornss  20973  isexid  20984  elghomlem1  21028  isrngo  21045  drngoi  21074  vci  21104  isvclem  21133  nvop2  21164  nvvop  21165  isnvlem  21166  dipfval  21275  sspval  21299  isssp  21300  lnoval  21330  nmoofval  21340  bloval  21359  0ofval  21365  ajfval  21387  hmoval  21388  isphg  21395  phop  21396  ipasslem11  21418  siii  21431  iscbn  21443  opsqrlem6  22725  elpjrn  22770  hstle1  22806  stm1addi  22825  stm1add3i  22827  mdslmd1lem1  22905  mdexchi  22915  atordi  22964  dmdbr5ati  23002  cdj3lem1  23014  feqmptdf  23228  xrofsup  23255  xpinpreima2  23291  xrge0mulc1cn  23323  disjabrex  23359  disjabrexf  23360  esumsn  23437  ofcc  23467  sxval  23521  measvuni  23542  itgmeq123dTMP  23589  totprob  23630  orrvcval4  23665  subfacp1lem5  23715  subfacp1lem6  23716  ispcon  23754  pconpi1  23768  rescon  23777  iscvm  23790  cvmsss2  23805  cvmliftlem3  23818  cvmliftlem5  23820  cvmliftlem10  23825  cvmliftlem11  23826  cvmlift2lem9a  23834  cvmlift2lem2  23835  cvmliftphtlem  23848  cvmlift3lem7  23856  umgraex  23875  vdgr1d  23894  eupath2lem3  23903  snmlflim  23915  ghomgrpilem2  23993  fz0n  24097  rdgprc  24151  dfrdg2  24152  dftrpred4g  24237  dfrdg4  24488  colinearalglem4  24537  axlowdimlem3  24572  axlowdimlem16  24585  axlowdimlem17  24586  fvline2  24769  ellines  24775  bpolylem  24783  bpoly1  24786  bpolydiflem  24789  rankeq1o  24801  ordcmp  24886  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem6  24930  dfoprab4pop  25037  fnovpop  25038  prjdmn  25082  prjrn  25083  mapex2  25140  repfuntw  25160  iscst1  25174  valcurfn1  25204  isorhom  25211  gepsup  25250  seinf  25251  mxlelt  25264  ltrcmp  25405  com2i  25416  idlvalNEW  25445  vri  25492  istopxc  25548  prdnei  25573  limptlimpr2lem2  25575  islimrs  25580  isalg  25721  algi  25727  isded  25736  dedi  25737  dedalg  25743  iscatOLD  25754  cati  25755  catded  25764  ishoma  25787  ismona  25809  isepia  25819  isiso  25825  cinvlem1  25828  isfuna  25834  issubcat  25845  linevala2  26078  isray2  26153  clsun  26246  isfne  26268  isref  26279  isptfin  26295  islocfin  26296  neibastop3  26311  cover2g  26359  f1opr  26391  sdclem1  26453  sstotbnd  26499  ssbnd  26512  prdstotbnd  26518  prdsbnd2  26519  ismtyhmeolem  26528  heiborlem3  26537  heiborlem4  26538  heiborlem6  26540  rrnval  26551  rrncmslem  26556  ismrer1  26562  reheibor  26563  rngohomval  26595  rngoisoval  26608  idlval  26638  pridlval  26658  maxidlval  26664  isprrngo  26675  igenval  26686  fndifnfp  26756  elrfi  26769  isnacs  26779  ofmpteq  26797  diophin  26852  dnnumch1  27141  islmodfg  27167  islnm  27175  lnmlssfg  27178  dsmmval  27200  dsmmbas2  27203  dsmmfi  27204  dsmm0cl  27206  frlmpws  27218  frlmlss  27219  frlmbas  27223  uvcfval  27233  frlmsplit2  27243  mapfien2  27258  frlmpwfi  27262  islindf  27282  lindfmm  27297  islindf5  27309  hbtlem1  27327  hbtlem7  27329  hbtlem6  27333  dgrnznn  27340  pmtrmvd  27398  pmtrfrn  27400  psgnunilem2  27418  psgnfval  27423  psgnghm2  27438  mamufval  27443  matval  27465  matplusg2  27477  matvsca2  27478  mdetfval  27487  mendval  27491  mendplusgfval  27493  mendmulrfval  27495  mendvscafval  27498  fgraphxp  27530  iotain  27617  rfcnpre1  27690  rfcnpre2  27702  rfcnpre3  27704  rfcnpre4  27705  fmuldfeq  27713  itgsinexplem1  27748  stoweidlem34  27783  stoweidlem41  27790  dfafn5a  28022  dfaimafn2  28028  ffnaov  28059  usgraexvlem  28127  1to2vfriswmgra  28184  dpval  28240  bnj66  28892  bnj570  28937  bnj1326  29056  bnj1463  29085  bnj1501  29097  lshpset  29168  lsatset  29180  lcvfbr  29210  lflset  29249  lkrfval  29277  lkrval2  29280  ldualset  29315  isopos  29370  cmtfvalN  29400  isoml  29428  cvrfval  29458  pats  29475  isatl  29489  iscvlat  29513  ishlat1  29542  llnset  29694  lplnset  29718  lvolset  29761  dalem58  29919  dalem59  29920  lineset  29927  pointsetN  29930  psubspset  29933  pmapfval  29945  paddfval  29986  pclfvalN  30078  polfvalN  30093  psubclsetN  30125  watfvalN  30181  lhpset  30184  lautset  30271  pautsetN  30287  ldilfset  30297  ltrnfset  30306  ltrnset  30307  ltrncoidN  30317  dilfsetN  30341  trnfsetN  30344  trlfset  30349  trlset  30350  cdleme6  30430  cdleme11g  30454  cdleme31sn1  30570  cdleme31sn1c  30577  cdleme31sn2  30578  cdleme40v  30658  cdleme42ke  30674  cdleme50trn2a  30739  cdleme50trn3  30742  cdlemg1b2  30760  cdlemg47  30925  tgrpfset  30933  tgrpset  30934  tendofset  30947  tendoset  30948  erngfset  30988  erngset  30989  erngfset-rN  30996  erngset-rN  30997  cdlemi  31009  cdlemk4  31023  cdlemkuu  31084  cdlemk35  31101  cdlemky  31115  cdlemk54  31147  cdlemk55a  31148  cdlemkyyN  31151  dva1dim  31174  erngdvlem3-rN  31187  dvafset  31193  dvaset  31194  diaffval  31220  diafval  31221  diaintclN  31248  dvhfset  31270  dvhset  31271  cdlemm10N  31308  docaffvalN  31311  docafvalN  31312  djaffvalN  31323  djafvalN  31324  dibffval  31330  dibfval  31331  dib1dim  31355  dibintclN  31357  dicffval  31364  dicfval  31365  dicval2  31369  dihffval  31420  dihfval  31421  dihopelvalcpre  31438  dihmeetbclemN  31494  dih1dimatlem  31519  dihglb2  31532  dihintcl  31534  dochffval  31539  dochfval  31540  djhffval  31586  djhfval  31587  dihjatcclem1  31608  dihjatcclem3  31610  djhlsmat  31617  lpolsetN  31672  lcdfval  31778  lcdval  31779  lcdval2  31780  lcdsca  31789  mapdffval  31816  mapdfval  31817  mapdval3N  31821  mapdval5N  31823  mapdpglem21  31882  hvmapffval  31948  hvmapfval  31949  hdmap1ffval  31986  hdmap1fval  31987  hdmapffval  32019  hdmapfval  32020  hgmapffval  32078  hgmapfval  32079  hdmapoc  32124  hlhilset  32127  hlhilslem  32131  hlhilnvl  32143
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-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator