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

Theorem syl6eqr 2437
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 2391 . 2  |-  B  =  C
41, 3syl6eq 2435 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  3eqtr4g  2444  iinrab2  4095  relop  4963  dfiun3g  5062  dfiin3g  5063  resima2  5119  relcnvfld  5340  uniabio  5368  iotanul  5373  fntpg  5446  dffn5  5711  dfimafn2  5715  fncnvima2  5791  fmptcof  5841  fcoconst  5844  fnpr  5889  fnprOLD  5890  resfunexg  5896  ffnov  6113  fnov  6117  fnrnov  6158  foov  6159  funimassov  6162  ovelimab  6163  ofc12  6268  caofinvl  6270  1st2val  6311  2nd2val  6312  curry1  6377  curry2  6380  dftpos3  6433  riotav  6490  riotauni  6492  tz7.44-3  6602  rdgsucmptnf  6623  rdglim2a  6627  frsucmptn  6632  seqomlem1  6643  seqomlem4  6646  oa0r  6718  om1r  6722  oarec  6741  oacomf1olem  6743  oeeulem  6780  omabs  6826  ecinxp  6915  mapunen  7212  phplem1  7222  fodomfi  7321  iinfi  7357  fiin  7362  dffi3  7371  ordtypelem3  7422  ordtypelem9  7428  cantnffval  7551  cantnfval  7556  cantnfp1lem3  7569  cantnflem1  7578  wemapwe  7587  oef1o  7588  cnfcom2lem  7591  rankuni  7722  cardval2  7811  dfac8alem  7843  dfac12lem1  7956  cda1dif  7989  cdaassen  7995  isf34lem4  8190  hsmexlem5  8243  axdc3lem4  8266  axdc4lem  8268  ac6num  8292  zorn2lem1  8309  ttukeylem3  8324  pwcfsdom  8391  fpwwe2lem9  8446  canth4  8455  canthp1lem2  8461  genpass  8819  prlem934  8843  mulcmpblnrlem  8881  recexsrlem  8911  supsrlem  8919  axrnegex  8970  nneo  10285  cnref1o  10539  xmulneg1  10780  xmulpnf1n  10789  xadddi  10806  fztp  11034  fseq1m1p1  11053  uzrdgsuci  11227  seqof2  11308  mulexpz  11347  expaddz  11351  bcp1m1  11538  hash1snb  11608  seqcoll  11639  iswrdi  11658  cjexp  11882  rexuz3  12079  limsupval  12195  limsupgle  12198  climconst  12264  zsum  12439  fsum  12441  sum0  12442  sumz  12443  fsumcnv  12484  mertenslem2  12589  efval2  12613  ege2le3  12619  efzval  12630  efival  12680  sinbnd  12708  cosbnd  12709  sadfval  12891  bitsres  12912  smufval  12916  smupp1  12919  eucalgval  13000  eucalginv  13002  eucalglt  13003  eucalgcvga  13004  eucalg  13005  dfphi2  13090  phimullem  13095  prmdiv  13101  odzval  13104  pcval  13145  pczpre  13148  pcrec  13159  prmreclem6  13216  4sqlem17  13256  vdwmc  13273  vdwpc  13275  vdwlem8  13283  ramval  13303  ramcl  13324  ressval  13443  resslem  13449  firest  13587  topnval  13589  prdsval  13605  prdsleval  13626  prdsbas3  13630  prdsdsval2  13633  pwsval  13635  pwsbas  13636  pwselbasb  13637  pwsplusgval  13639  pwsmulrval  13640  pwsle  13641  pwsvscafval  13643  imasval  13664  imasdsval  13668  imasdsval2  13669  divsval  13694  xpsval  13724  xpslem  13725  xpsaddlem  13727  xpsvsca  13731  xpsle  13733  mrisval  13782  iscat  13824  cidfval  13828  homffval  13844  comfffval  13851  comffval  13852  comfeq  13859  oppcval  13866  oppchomfval  13867  oppccofval  13869  oppcid  13874  monfval  13885  oppcmon  13891  sectffval  13903  invffval  13910  isoval  13917  isssc  13947  reschomf  13958  issubc  13962  isfunc  13988  isfuncd  13989  funcf2  13992  idfuval  14000  idfu2nd  14001  cofucl  14012  resfval2  14017  resf2nd  14019  funcres2b  14021  funcpropd  14024  isfull  14034  isfth  14038  natfval  14070  fucval  14082  homafval  14111  homaval  14113  homadmcd  14124  arwval  14125  arwhoma  14127  idafval  14139  coafval  14146  coapm  14153  catcco  14183  catcid  14185  catcisolem  14188  xpcval  14201  xpcco  14207  1stfval  14215  2ndfval  14218  xpcpropd  14232  evlfval  14241  evlfcllem  14245  evlfcl  14246  curfval  14247  curf1cl  14252  curfcl  14256  uncf1  14260  uncf2  14261  uncfcurf  14263  diag2  14269  curf2ndf  14271  hofval  14276  hof2fval  14279  hofcl  14283  yonval  14285  hofpropd  14291  yonedalem21  14297  yonedalem22  14302  yonedalem3  14304  yonedainv  14305  yonffthlem  14306  isdrs  14318  ispos  14331  pltfval  14343  lubfval  14362  glbfval  14367  joinfval  14371  meetfval  14378  p0val  14397  p1val  14398  islat  14403  isclat  14465  ipoval  14507  isipodrs  14514  isdlat  14546  istsr  14576  spwval2  14583  isla  14592  isdir  14604  ismnd  14619  plusffval  14629  grpidval  14634  ismgmid  14637  pws0g  14658  ismhm  14667  submacs  14692  gsumvalx  14701  frmdval  14723  isgrp  14743  grpn0  14764  grpinvfval  14770  grpsubfval  14774  mulgfval  14818  mulgval  14819  mulgnn0p1  14828  pwsinvg  14857  issubg  14871  isnsg  14896  eqgfval  14915  divseccl  14923  isghm  14933  conjsubg  14964  conjsubgen  14965  isgim  14976  isga  14995  symgval  15021  cntrval  15045  cntzfval  15046  oppgval  15070  invoppggim  15083  odfval  15098  odval  15099  gexval  15139  ispgp  15153  sylow1lem1  15159  slwispgp  15172  pgpssslw  15175  sylow2alem2  15179  sylow3lem5  15192  lsmfval  15199  pj1fval  15253  efgmnvl  15273  efgval  15276  efgval2  15283  efginvrel2  15286  efgsfo  15298  efgredleme  15302  efgredlemd  15303  efgredlemc  15304  frgpval  15317  frgpeccl  15320  vrgpfval  15325  frgpuptinv  15330  frgpup3lem  15336  iscmn  15346  subcmn  15383  frgpnabllem1  15411  iscyg  15416  lt6abl  15431  gsumval3  15441  gsumzf1o  15446  gsum2d  15473  gsumcom2  15476  dmdprd  15486  dprdval  15488  dprd2da  15527  dmdprdsplit2lem  15530  dpjfval  15540  pgpfaclem1  15566  mgpval  15578  mgpplusg  15579  isrng  15595  iscrng  15598  pws1  15649  opprval  15656  crngoppr  15659  dvdsrval  15677  isunit  15689  invrfval  15705  dvrfval  15716  isirred  15731  dfrhm2  15748  pwsco1rhm  15760  pwsco2rhm  15761  isdrng  15766  isdrng2  15772  drngid  15776  isdrngrd  15788  issubrg  15795  abvfval  15833  abvneg  15849  staffval  15862  issrng  15865  issrngd  15876  islmod  15881  scaffval  15895  lssset  15937  prdsvscacl  15971  lspfval  15976  islmhm  16030  islmhm2  16041  islmim  16061  islbs  16075  islvec  16103  2idlval  16231  crng2idl  16237  isnzr  16257  rrgval  16274  isdomn  16281  isassa  16302  aspval  16314  asclfval  16320  psrval  16356  mvrfval  16411  mplval  16419  mplcoe3  16456  mplcoe2  16457  ltbval  16459  opsrval  16462  mplind  16489  vr1cl2  16518  ply1val  16519  psropprmul  16559  coe1mul2lem2  16588  coe1tm  16592  coe1sclmul  16601  coe1sclmul2  16603  ply1scl1  16610  ply1coe  16611  mulgrhm2  16711  zlmval  16720  chrval  16729  znval  16739  znzrhfo  16751  znle2  16757  znunithash  16768  cygznlem1  16770  isphl  16782  phllmhm  16786  ipffval  16802  ocvfval  16816  cssval  16832  cssincl  16838  thlval  16845  pjfval  16856  ishil  16868  isobs  16870  istps  16924  cldval  17010  ntrfval  17011  clsfval  17012  neifval  17086  lpfval  17125  isperf  17137  restbas  17144  tgrest  17145  resstopn  17172  ordtval  17175  ordtuni  17176  ordtbas  17178  ordtrest2  17190  ist0  17306  ist1  17307  ishaus  17308  iscnrm  17309  pnrmopn  17329  iscmp  17373  cmpcld  17387  hauscmplem  17391  cmpfi  17393  iscon  17397  consuba  17404  is1stc  17425  txval  17517  ptval  17523  ptbasin  17530  ptbasfi  17534  xkoval  17540  ptunimpt  17548  ptval2  17554  txbasval  17559  dfac14  17571  upxp  17576  uptx  17578  prdstopn  17581  txrest  17584  ptrescn  17592  lmcn2  17602  xkoptsub  17607  xkopt  17608  xkococn  17613  cnmpt2t  17626  cnmpt2res  17630  cnmpt2k  17641  imasnopn  17643  imasncld  17644  imasncls  17645  qtopval  17648  imastopn  17673  hmphindis  17750  ptuncnv  17760  ptunhmeo  17761  xpstopnlem1  17762  xpstopnlem2  17764  xkohmeo  17768  qtophmeo  17770  elmptrab  17780  trfbas2  17796  trfil2  17840  fmco  17914  flimval  17916  flfcnp2  17960  fclsval  17961  fclsrest  17977  alexsublem  17996  alexsubALTlem3  18001  alexsubALTlem4  18002  ptcmplem1  18004  ptcmplem3  18006  ptcmpg  18009  istmd  18025  istgp  18028  istgp2  18042  tgplacthmeo  18054  clssubg  18059  tgpconcompeqg  18062  tsmsval2  18080  istrg  18114  istdrg  18116  istlm  18135  istvc  18142  ustbas  18178  trust  18180  ustuqtop1  18192  ustuqtop2  18193  utopsnneiplem  18198  utop2nei  18201  utop3cls  18202  utopreg  18203  isusp  18212  imasdsf1olem  18311  xpsxmetlem  18317  xpsmet  18320  isxms  18367  isms  18369  tmsval  18401  stdbdxmet  18435  prdsxmslem2  18449  txmetcnp  18467  nmfval  18507  isngp  18514  tngval  18551  tngtopn  18562  tngnm  18563  isnrg  18567  isnlm  18582  nmofval  18619  nghmfval  18627  qtopbaslem  18663  cnblcld  18680  negcncf  18819  negfcncf  18820  cncfcnvcn  18822  cnmptre  18823  cnheiborlem  18850  cnheibor  18851  bndth  18854  pcorev2  18924  om1bas  18927  pi1val  18933  pi1bas3  18939  pi1cpbl  18940  pi1xfrcnv  18953  isclm  18960  nmoleub2lem3  18994  nmoleub3  18998  iscph  19004  cphcjcl  19017  tchval  19048  ipcau2  19062  csscld  19074  iscmet  19108  caubl  19131  caublcls  19132  bcthlem4  19149  bcthlem5  19150  bcth3  19153  isbn  19160  iscms  19167  ovolfioo  19231  ovolficc  19232  ovolficcss  19233  ovolfsval  19234  ovolval  19237  ovollb2lem  19251  ovolctb  19253  ovolunlem1a  19259  ovoliunlem1  19265  ovoliun2  19269  shft2rab  19271  ovolshftlem1  19272  sca2rab  19275  ovolscalem1  19276  ovolicc2lem1  19280  ovolicc2lem4  19283  ovolicc2lem5  19284  cmmbl  19296  unmbl  19299  voliunlem3  19313  iunmbl  19314  voliun  19315  ioombl1lem3  19321  ovolfs2  19330  ioorinv  19335  uniiccdif  19337  uniioovol  19338  uniioombllem2a  19341  uniioombllem2  19342  uniioombllem3a  19343  uniioombllem3  19344  uniioombllem4  19345  uniioombllem5  19346  uniioombllem6  19347  dyadovol  19352  dyadss  19353  dyaddisjlem  19354  dyadmaxlem  19356  dyadmbl  19359  opnmbllem  19360  vitalilem4  19370  ismbf  19389  mbfconst  19394  itg2val  19487  itg2monolem1  19509  itg2i1fseq  19514  dfitg  19528  itgz  19539  itgvallem3  19544  iblcnlem1  19546  iblcnlem  19547  iblposlem  19550  itgreval  19555  itgfsum  19585  bddmulibl  19597  itgcn  19601  limcfval  19626  ellimc  19627  limcmpt2  19638  limccnp  19645  dvfval  19651  eldv  19652  dvreslem  19663  dvres2lem  19664  dvidlem  19669  dvnfval  19675  dvexp2  19707  dvrec  19708  dveflem  19730  dvlipcn  19745  dv11cn  19752  lhop  19767  ftc2  19795  evlsval  19807  evlsval2  19808  evlval  19812  evlrhm  19813  evl1fval  19814  evl1sca  19817  evl1var  19819  pf1subrg  19835  pf1ind  19842  mdegfval  19852  uc1pval  19929  mon1pval  19931  q1pval  19943  r1pval  19946  ig1pval  19962  plyconst  19992  plyeq0lem  19996  dgrval  20014  plyco  20027  0dgrb  20032  coemullem  20035  coe0  20041  coesub  20042  dgrsub  20057  dgrcolem1  20058  dgrcolem2  20059  dgrco  20060  quotval  20076  plydivex  20081  quotlem  20084  plyremlem  20088  fta1  20092  vieta1lem1  20094  vieta1lem2  20095  vieta1  20096  aaliou2  20124  aaliou3lem7  20133  taylpfval  20148  dvtaylp  20153  dvntaylp0  20155  taylthlem1  20156  ulm2  20168  ulmshft  20173  pserdvlem2  20211  abelthlem1  20214  abelthlem8  20222  abelth  20224  abelth2  20225  ptolemy  20271  coskpi  20295  efif1olem2  20312  efif1olem3  20313  logcnlem4  20403  advlogexp  20413  efopn  20416  logtayl  20418  dcubic2  20551  dcubic  20553  quart1lem  20562  atancj  20617  tanatan  20626  cosatan  20628  dvatan  20642  leibpi  20649  birthdaylem2  20658  efrlim  20675  emcllem7  20707  wilthlem2  20719  basellem5  20734  basellem8  20737  basellem9  20738  vmaval  20763  prmorcht  20828  mumul  20831  dvdsmulf1o  20846  fsumdvdsmul  20847  ppiub  20855  fsumvma  20864  pclogsum  20866  dchrval  20885  bposlem8  20942  lgslem1  20947  lgsval  20951  lgsval4  20967  lgsfcl3  20968  lgsdilem  20973  lgsdir2lem4  20977  lgsdir2lem5  20978  lgsquadlem2  21006  dchrisum0flb  21071  rpvmasum2  21073  log2sumbnd  21105  selberglem2  21107  pntibndlem2  21152  pntlemp  21171  ostth2lem3  21196  ostth2lem4  21197  umgraex  21225  usgraexvlem  21280  nbgraf1olem5  21321  constr3trllem3  21487  constr3cycllem1  21493  vdgr1d  21522  eupath2lem3  21549  isplig  21613  gidval  21649  grpoinvfval  21660  grpodivfval  21678  gxfval  21693  isablo  21719  subgornss  21742  isexid  21753  elghomlem1  21797  isrngo  21814  drngoi  21843  vci  21875  isvclem  21904  nvop2  21935  nvvop  21936  isnvlem  21937  dipfval  22046  sspval  22070  isssp  22071  lnoval  22101  nmoofval  22111  bloval  22130  0ofval  22136  ajfval  22158  hmoval  22159  isphg  22166  phop  22167  ipasslem11  22189  siii  22202  iscbn  22214  opsqrlem6  23496  elpjrn  23541  hstle1  23577  stm1addi  23596  stm1add3i  23598  mdslmd1lem1  23676  mdexchi  23686  atordi  23735  dmdbr5ati  23773  cdj3lem1  23785  disjabrex  23868  disjabrexf  23869  csbcnvg  23880  feqmptdf  23917  xrofsup  23962  isofld  24061  subofld  24071  xpinpreima2  24109  zlmds  24149  qqhval  24157  rrhval  24178  esumsn  24252  ofcc  24285  sxval  24340  measvuni  24362  volmeas  24381  elunirnmbfm  24397  totprob  24464  orrvcval4  24501  lgamcvglem  24603  subfacp1lem5  24649  subfacp1lem6  24650  ispcon  24689  pconpi1  24703  rescon  24712  iscvm  24725  cvmsss2  24740  cvmliftlem3  24753  cvmliftlem5  24755  cvmliftlem10  24760  cvmliftlem11  24761  cvmlift2lem9a  24769  cvmlift2lem2  24770  cvmliftphtlem  24783  cvmlift3lem7  24791  snmlflim  24798  ghomgrpilem2  24876  fz0n  24981  zprod  25042  fprod  25046  prod0  25048  prod1  25049  fallfacfwd  25119  rdgprc  25175  dfrdg2  25176  dftrpred4g  25261  dfrdg4  25513  colinearalglem4  25562  axlowdimlem3  25597  axlowdimlem16  25610  axlowdimlem17  25611  fvline2  25794  ellines  25800  bpolylem  25808  bpoly1  25811  bpolydiflem  25814  rankeq1o  25826  ordcmp  25911  volsupnfl  25956  itg2addnclem  25957  itgaddnclem2  25964  dvreasin  25980  dvreacos  25981  areacirclem2  25982  areacirclem6  25987  clsun  26022  isfne  26039  isref  26050  isptfin  26066  islocfin  26067  neibastop3  26082  cover2g  26107  f1opr  26117  sdclem1  26138  sstotbnd  26175  ssbnd  26188  prdstotbnd  26194  prdsbnd2  26195  ismtyhmeolem  26204  heiborlem3  26213  heiborlem4  26214  heiborlem6  26216  rrnval  26227  rrncmslem  26232  ismrer1  26238  reheibor  26239  rngohomval  26271  rngoisoval  26284  idlval  26314  pridlval  26334  maxidlval  26340  isprrngo  26351  igenval  26362  fndifnfp  26428  elrfi  26439  isnacs  26449  ofmpteq  26467  diophin  26522  dnnumch1  26810  islmodfg  26836  islnm  26844  lnmlssfg  26847  dsmmval  26869  dsmmbas2  26872  dsmmfi  26873  dsmm0cl  26875  frlmpws  26887  frlmlss  26888  frlmbas  26892  uvcfval  26902  frlmsplit2  26912  mapfien2  26927  frlmpwfi  26931  islindf  26951  lindfmm  26966  islindf5  26978  hbtlem1  26996  hbtlem7  26998  hbtlem6  27002  dgrnznn  27009  pmtrmvd  27067  pmtrfrn  27069  psgnunilem2  27087  psgnfval  27092  psgnghm2  27107  mamufval  27112  matval  27134  matplusg2  27146  matvsca2  27147  mdetfval  27156  mendval  27160  mendplusgfval  27162  mendmulrfval  27164  mendvscafval  27167  fgraphxp  27199  iotain  27286  rfcnpre1  27358  rfcnpre2  27370  rfcnpre3  27372  rfcnpre4  27373  fmuldfeq  27381  stoweidlem34  27451  stoweidlem41  27458  stirlinglem7  27497  dfafn5a  27693  dfaimafn2  27699  ffnaov  27732  1to2vfriswmgra  27759  dpval  27859  bnj66  28569  bnj570  28614  bnj1326  28733  bnj1463  28762  bnj1501  28774  lshpset  29093  lsatset  29105  lcvfbr  29135  lflset  29174  lkrfval  29202  lkrval2  29205  ldualset  29240  isopos  29295  cmtfvalN  29325  isoml  29353  cvrfval  29383  pats  29400  isatl  29414  iscvlat  29438  ishlat1  29467  llnset  29619  lplnset  29643  lvolset  29686  dalem58  29844  dalem59  29845  lineset  29852  pointsetN  29855  psubspset  29858  pmapfval  29870  paddfval  29911  pclfvalN  30003  polfvalN  30018  psubclsetN  30050  watfvalN  30106  lhpset  30109  lautset  30196  pautsetN  30212  ldilfset  30222  ltrnfset  30231  ltrnset  30232  ltrncoidN  30242  dilfsetN  30266  trnfsetN  30269  trlfset  30274  trlset  30275  cdleme6  30355  cdleme11g  30379  cdleme31sn1  30495  cdleme31sn1c  30502  cdleme31sn2  30503  cdleme40v  30583  cdleme42ke  30599  cdleme50trn2a  30664  cdleme50trn3  30667  cdlemg1b2  30685  cdlemg47  30850  tgrpfset  30858  tgrpset  30859  tendofset  30872  tendoset  30873  erngfset  30913  erngset  30914  erngfset-rN  30921  erngset-rN  30922  cdlemi  30934  cdlemk4  30948  cdlemkuu  31009  cdlemk35  31026  cdlemky  31040  cdlemk54  31072  cdlemk55a  31073  cdlemkyyN  31076  dva1dim  31099  erngdvlem3-rN  31112  dvafset  31118  dvaset  31119  diaffval  31145  diafval  31146  diaintclN  31173  dvhfset  31195  dvhset  31196  cdlemm10N  31233  docaffvalN  31236  docafvalN  31237  djaffvalN  31248  djafvalN  31249  dibffval  31255  dibfval  31256  dib1dim  31280  dibintclN  31282  dicffval  31289  dicfval  31290  dicval2  31294  dihffval  31345  dihfval  31346  dihopelvalcpre  31363  dihmeetbclemN  31419  dih1dimatlem  31444  dihglb2  31457  dihintcl  31459  dochffval  31464  dochfval  31465  djhffval  31511  djhfval  31512  dihjatcclem1  31533  dihjatcclem3  31535  djhlsmat  31542  lpolsetN  31597  lcdfval  31703  lcdval  31704  lcdval2  31705  lcdsca  31714  mapdffval  31741  mapdfval  31742  mapdval3N  31746  mapdval5N  31748  mapdpglem21  31807  hvmapffval  31873  hvmapfval  31874  hdmap1ffval  31911  hdmap1fval  31912  hdmapffval  31944  hdmapfval  31945  hgmapffval  32003  hgmapfval  32004  hdmapoc  32049  hlhilset  32052  hlhilslem  32056  hlhilnvl  32068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2380
  Copyright terms: Public domain W3C validator