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

Theorem syl6eqr 2487
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 2441 . 2  |-  B  =  C
41, 3syl6eq 2485 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  3eqtr4g  2494  iinrab2  4155  relop  5024  dfiun3g  5123  dfiin3g  5124  resima2  5180  relcnvfld  5401  uniabio  5429  iotanul  5434  fntpg  5507  dffn5  5773  dfimafn2  5777  fncnvima2  5853  fmptcof  5903  fcoconst  5906  fnpr  5951  fnprOLD  5952  resfunexg  5958  ffnov  6175  fnov  6179  fnrnov  6220  foov  6221  funimassov  6224  ovelimab  6225  ofc12  6330  caofinvl  6332  1st2val  6373  2nd2val  6374  curry1  6439  curry2  6442  dftpos3  6498  riotav  6555  riotauni  6557  tz7.44-3  6667  rdgsucmptnf  6688  rdglim2a  6692  frsucmptn  6697  seqomlem1  6708  seqomlem4  6711  oa0r  6783  om1r  6787  oarec  6806  oacomf1olem  6808  oeeulem  6845  omabs  6891  ecinxp  6980  mapunen  7277  phplem1  7287  fodomfi  7386  iinfi  7423  fiin  7428  dffi3  7437  ordtypelem3  7490  ordtypelem9  7496  cantnffval  7619  cantnfval  7624  cantnfp1lem3  7637  cantnflem1  7646  wemapwe  7655  oef1o  7656  cnfcom2lem  7659  rankuni  7790  cardval2  7879  dfac8alem  7911  dfac12lem1  8024  cda1dif  8057  cdaassen  8063  isf34lem4  8258  hsmexlem5  8311  axdc3lem4  8334  axdc4lem  8336  ac6num  8360  zorn2lem1  8377  ttukeylem3  8392  pwcfsdom  8459  fpwwe2lem9  8514  canth4  8523  canthp1lem2  8529  genpass  8887  prlem934  8911  mulcmpblnrlem  8949  recexsrlem  8979  supsrlem  8987  axrnegex  9038  nneo  10354  cnref1o  10608  xmulneg1  10849  xmulpnf1n  10858  xadddi  10875  fztp  11103  fseq1m1p1  11124  uzrdgsuci  11301  seqof2  11382  mulexpz  11421  expaddz  11425  bcp1m1  11612  hash1snb  11682  seqcoll  11713  iswrdi  11732  cjexp  11956  rexuz3  12153  limsupval  12269  limsupgle  12272  climconst  12338  zsum  12513  fsum  12515  sum0  12516  sumz  12517  fsumcnv  12558  mertenslem2  12663  efval2  12687  ege2le3  12693  efzval  12704  efival  12754  sinbnd  12782  cosbnd  12783  sadfval  12965  bitsres  12986  smufval  12990  smupp1  12993  eucalgval  13074  eucalginv  13076  eucalglt  13077  eucalgcvga  13078  eucalg  13079  dfphi2  13164  phimullem  13169  prmdiv  13175  odzval  13178  pcval  13219  pczpre  13222  pcrec  13233  prmreclem6  13290  4sqlem17  13330  vdwmc  13347  vdwpc  13349  vdwlem8  13357  ramval  13377  ramcl  13398  ressval  13517  resslem  13523  firest  13661  topnval  13663  prdsval  13679  prdsleval  13700  prdsbas3  13704  prdsdsval2  13707  pwsval  13709  pwsbas  13710  pwselbasb  13711  pwsplusgval  13713  pwsmulrval  13714  pwsle  13715  pwsvscafval  13717  imasval  13738  imasdsval  13742  imasdsval2  13743  divsval  13768  xpsval  13798  xpslem  13799  xpsaddlem  13801  xpsvsca  13805  xpsle  13807  mrisval  13856  iscat  13898  cidfval  13902  homffval  13918  comfffval  13925  comffval  13926  comfeq  13933  oppcval  13940  oppchomfval  13941  oppccofval  13943  oppcid  13948  monfval  13959  oppcmon  13965  sectffval  13977  invffval  13984  isoval  13991  isssc  14021  reschomf  14032  issubc  14036  isfunc  14062  isfuncd  14063  funcf2  14066  idfuval  14074  idfu2nd  14075  cofucl  14086  resfval2  14091  resf2nd  14093  funcres2b  14095  funcpropd  14098  isfull  14108  isfth  14112  natfval  14144  fucval  14156  homafval  14185  homaval  14187  homadmcd  14198  arwval  14199  arwhoma  14201  idafval  14213  coafval  14220  coapm  14227  catcco  14257  catcid  14259  catcisolem  14262  xpcval  14275  xpcco  14281  1stfval  14289  2ndfval  14292  xpcpropd  14306  evlfval  14315  evlfcllem  14319  evlfcl  14320  curfval  14321  curf1cl  14326  curfcl  14330  uncf1  14334  uncf2  14335  uncfcurf  14337  diag2  14343  curf2ndf  14345  hofval  14350  hof2fval  14353  hofcl  14357  yonval  14359  hofpropd  14365  yonedalem21  14371  yonedalem22  14376  yonedalem3  14378  yonedainv  14379  yonffthlem  14380  isdrs  14392  ispos  14405  pltfval  14417  lubfval  14436  glbfval  14441  joinfval  14445  meetfval  14452  p0val  14471  p1val  14472  islat  14477  isclat  14539  ipoval  14581  isipodrs  14588  isdlat  14620  istsr  14650  spwval2  14657  isla  14666  isdir  14678  ismnd  14693  plusffval  14703  grpidval  14708  ismgmid  14711  pws0g  14732  ismhm  14741  submacs  14766  gsumvalx  14775  frmdval  14797  isgrp  14817  grpn0  14838  grpinvfval  14844  grpsubfval  14848  mulgfval  14892  mulgval  14893  mulgnn0p1  14902  pwsinvg  14931  issubg  14945  isnsg  14970  eqgfval  14989  divseccl  14997  isghm  15007  conjsubg  15038  conjsubgen  15039  isgim  15050  isga  15069  symgval  15095  cntrval  15119  cntzfval  15120  oppgval  15144  invoppggim  15157  odfval  15172  odval  15173  gexval  15213  ispgp  15227  sylow1lem1  15233  slwispgp  15246  pgpssslw  15249  sylow2alem2  15253  sylow3lem5  15266  lsmfval  15273  pj1fval  15327  efgmnvl  15347  efgval  15350  efgval2  15357  efginvrel2  15360  efgsfo  15372  efgredleme  15376  efgredlemd  15377  efgredlemc  15378  frgpval  15391  frgpeccl  15394  vrgpfval  15399  frgpuptinv  15404  frgpup3lem  15410  iscmn  15420  subcmn  15457  frgpnabllem1  15485  iscyg  15490  lt6abl  15505  gsumval3  15515  gsumzf1o  15520  gsum2d  15547  gsumcom2  15550  dmdprd  15560  dprdval  15562  dprd2da  15601  dmdprdsplit2lem  15604  dpjfval  15614  pgpfaclem1  15640  mgpval  15652  mgpplusg  15653  isrng  15669  iscrng  15672  pws1  15723  opprval  15730  crngoppr  15733  dvdsrval  15751  isunit  15763  invrfval  15779  dvrfval  15790  isirred  15805  dfrhm2  15822  pwsco1rhm  15834  pwsco2rhm  15835  isdrng  15840  isdrng2  15846  drngid  15850  isdrngrd  15862  issubrg  15869  abvfval  15907  abvneg  15923  staffval  15936  issrng  15939  issrngd  15950  islmod  15955  scaffval  15969  lssset  16011  prdsvscacl  16045  lspfval  16050  islmhm  16104  islmhm2  16115  islmim  16135  islbs  16149  islvec  16177  2idlval  16305  crng2idl  16311  isnzr  16331  rrgval  16348  isdomn  16355  isassa  16376  aspval  16388  asclfval  16394  psrval  16430  mvrfval  16485  mplval  16493  mplcoe3  16530  mplcoe2  16531  ltbval  16533  opsrval  16536  mplind  16563  vr1cl2  16592  ply1val  16593  psropprmul  16633  coe1mul2lem2  16662  coe1tm  16666  coe1sclmul  16675  coe1sclmul2  16677  ply1scl1  16684  ply1coe  16685  mulgrhm2  16789  zlmval  16798  chrval  16807  znval  16817  znzrhfo  16829  znle2  16835  znunithash  16846  cygznlem1  16848  isphl  16860  phllmhm  16864  ipffval  16880  ocvfval  16894  cssval  16910  cssincl  16916  thlval  16923  pjfval  16934  ishil  16946  isobs  16948  istps  17002  cldval  17088  ntrfval  17089  clsfval  17090  neifval  17164  lpfval  17203  isperf  17216  restbas  17223  tgrest  17224  resstopn  17251  ordtval  17254  ordtuni  17255  ordtbas  17257  ordtrest2  17269  ist0  17385  ist1  17386  ishaus  17387  iscnrm  17388  pnrmopn  17408  iscmp  17452  cmpcld  17466  hauscmplem  17470  cmpfi  17472  iscon  17477  consuba  17484  is1stc  17505  txval  17597  ptval  17603  ptbasin  17610  ptbasfi  17614  xkoval  17620  ptunimpt  17628  ptval2  17634  txbasval  17639  dfac14  17651  upxp  17656  uptx  17658  prdstopn  17661  txrest  17664  ptrescn  17672  lmcn2  17682  xkoptsub  17687  xkopt  17688  xkococn  17693  cnmpt2t  17706  cnmpt2res  17710  cnmpt2k  17721  imasnopn  17723  imasncld  17724  imasncls  17725  qtopval  17728  imastopn  17753  hmphindis  17830  ptuncnv  17840  ptunhmeo  17841  xpstopnlem1  17842  xpstopnlem2  17844  xkohmeo  17848  qtophmeo  17850  elmptrab  17860  trfbas2  17876  trfil2  17920  fmco  17994  flimval  17996  flfcnp2  18040  fclsval  18041  fclsrest  18057  alexsublem  18076  alexsubALTlem3  18081  alexsubALTlem4  18082  ptcmplem1  18084  ptcmplem3  18086  ptcmpg  18089  istmd  18105  istgp  18108  istgp2  18122  tgplacthmeo  18134  clssubg  18139  tgpconcompeqg  18142  tsmsval2  18160  istrg  18194  istdrg  18196  istlm  18215  istvc  18222  ustbas  18258  trust  18260  ustuqtop1  18272  ustuqtop2  18273  utopsnneiplem  18278  utop2nei  18281  utop3cls  18282  utopreg  18283  isusp  18292  psmetxrge0  18345  imasdsf1olem  18404  xpsxmetlem  18410  xpsmet  18413  isxms  18478  isms  18480  tmsval  18512  stdbdxmet  18546  prdsxmslem2  18560  txmetcnp  18578  nmfval  18637  isngp  18644  tngval  18681  tngtopn  18692  tngnm  18693  isnrg  18697  isnlm  18712  nmofval  18749  nghmfval  18757  qtopbaslem  18793  cnblcld  18810  negcncf  18949  negfcncf  18950  cncfcnvcn  18952  cnmptre  18953  cnheiborlem  18980  cnheibor  18981  bndth  18984  pcorev2  19054  om1bas  19057  pi1val  19063  pi1bas3  19069  pi1cpbl  19070  pi1xfrcnv  19083  isclm  19090  nmoleub2lem3  19124  nmoleub3  19128  iscph  19134  cphcjcl  19147  tchval  19178  ipcau2  19192  csscld  19204  iscmet  19238  caubl  19261  caublcls  19262  bcthlem4  19281  bcthlem5  19282  bcth3  19285  isbn  19292  iscms  19299  ovolfioo  19365  ovolficc  19366  ovolficcss  19367  ovolfsval  19368  ovolval  19371  ovollb2lem  19385  ovolctb  19387  ovolunlem1a  19393  ovoliunlem1  19399  ovoliun2  19403  shft2rab  19405  ovolshftlem1  19406  sca2rab  19409  ovolscalem1  19410  ovolicc2lem1  19414  ovolicc2lem4  19417  ovolicc2lem5  19418  cmmbl  19430  unmbl  19433  voliunlem3  19447  iunmbl  19448  voliun  19449  ioombl1lem3  19455  ovolfs2  19464  ioorinv  19469  uniiccdif  19471  uniioovol  19472  uniioombllem2a  19475  uniioombllem2  19476  uniioombllem3a  19477  uniioombllem3  19478  uniioombllem4  19479  uniioombllem5  19480  uniioombllem6  19481  dyadovol  19486  dyadss  19487  dyaddisjlem  19488  dyadmaxlem  19490  dyadmbl  19493  opnmbllem  19494  vitalilem4  19504  ismbf  19523  mbfconst  19528  itg2val  19621  itg2monolem1  19643  itg2i1fseq  19648  dfitg  19662  itgz  19673  itgvallem3  19678  iblcnlem1  19680  iblcnlem  19681  iblposlem  19684  itgreval  19689  itgfsum  19719  bddmulibl  19731  itgcn  19735  limcfval  19760  ellimc  19761  limcmpt2  19772  limccnp  19779  dvfval  19785  eldv  19786  dvreslem  19797  dvres2lem  19798  dvidlem  19803  dvnfval  19809  dvexp2  19841  dvrec  19842  dveflem  19864  dvlipcn  19879  dv11cn  19886  lhop  19901  ftc2  19929  evlsval  19941  evlsval2  19942  evlval  19946  evlrhm  19947  evl1fval  19948  evl1sca  19951  evl1var  19953  pf1subrg  19969  pf1ind  19976  mdegfval  19986  uc1pval  20063  mon1pval  20065  q1pval  20077  r1pval  20080  ig1pval  20096  plyconst  20126  plyeq0lem  20130  dgrval  20148  plyco  20161  0dgrb  20166  coemullem  20169  coe0  20175  coesub  20176  dgrsub  20191  dgrcolem1  20192  dgrcolem2  20193  dgrco  20194  quotval  20210  plydivex  20215  quotlem  20218  plyremlem  20222  fta1  20226  vieta1lem1  20228  vieta1lem2  20229  vieta1  20230  aaliou2  20258  aaliou3lem7  20267  taylpfval  20282  dvtaylp  20287  dvntaylp0  20289  taylthlem1  20290  ulm2  20302  ulmshft  20307  pserdvlem2  20345  abelthlem1  20348  abelthlem8  20356  abelth  20358  abelth2  20359  ptolemy  20405  coskpi  20429  efif1olem2  20446  efif1olem3  20447  logcnlem4  20537  advlogexp  20547  efopn  20550  logtayl  20552  dcubic2  20685  dcubic  20687  quart1lem  20696  atancj  20751  tanatan  20760  cosatan  20762  dvatan  20776  leibpi  20783  birthdaylem2  20792  efrlim  20809  emcllem7  20841  wilthlem2  20853  basellem5  20868  basellem8  20871  basellem9  20872  vmaval  20897  prmorcht  20962  mumul  20965  dvdsmulf1o  20980  fsumdvdsmul  20981  ppiub  20989  fsumvma  20998  pclogsum  21000  dchrval  21019  bposlem8  21076  lgslem1  21081  lgsval  21085  lgsval4  21101  lgsfcl3  21102  lgsdilem  21107  lgsdir2lem4  21111  lgsdir2lem5  21112  lgsquadlem2  21140  dchrisum0flb  21205  rpvmasum2  21207  log2sumbnd  21239  selberglem2  21241  pntibndlem2  21286  pntlemp  21305  ostth2lem3  21330  ostth2lem4  21331  umgraex  21359  usgraexvlem  21415  nbgraf1olem5  21456  constr3trllem3  21640  constr3cycllem1  21646  vdgr1d  21675  eupath2lem3  21702  isplig  21766  gidval  21802  grpoinvfval  21813  grpodivfval  21831  gxfval  21846  isablo  21872  subgornss  21895  isexid  21906  elghomlem1  21950  isrngo  21967  drngoi  21996  vci  22028  isvclem  22057  nvop2  22088  nvvop  22089  isnvlem  22090  dipfval  22199  sspval  22223  isssp  22224  lnoval  22254  nmoofval  22264  bloval  22283  0ofval  22289  ajfval  22311  hmoval  22312  isphg  22319  phop  22320  ipasslem11  22342  siii  22355  iscbn  22367  opsqrlem6  23649  elpjrn  23694  hstle1  23730  stm1addi  23749  stm1add3i  23751  mdslmd1lem1  23829  mdexchi  23839  atordi  23888  dmdbr5ati  23926  cdj3lem1  23938  disjabrex  24025  disjabrexf  24026  csbcnvg  24038  feqmptdf  24076  xrofsup  24127  isofld  24236  subofld  24246  inftmrel  24251  isinftm  24252  pstmfval  24292  xpinpreima2  24306  zlmds  24349  qqhval  24359  rrhval  24380  xrhval  24385  esumsn  24457  ofcc  24490  sxval  24545  measvuni  24569  volmeas  24588  elunirnmbfm  24604  sitgval  24648  sibfof  24655  sitgclcn  24659  sitgclre  24660  totprob  24686  orrvcval4  24723  lgamcvglem  24825  subfacp1lem5  24871  subfacp1lem6  24872  ispcon  24911  pconpi1  24925  rescon  24934  iscvm  24947  cvmsss2  24962  cvmliftlem3  24975  cvmliftlem5  24977  cvmliftlem10  24982  cvmliftlem11  24983  cvmlift2lem9a  24991  cvmlift2lem2  24992  cvmliftphtlem  25005  cvmlift3lem7  25013  snmlflim  25020  ghomgrpilem2  25098  fz0n  25203  zprod  25264  fprod  25268  prod0  25270  prod1  25271  fprodcnv  25308  fallfacfwd  25353  binomfallfaclem2  25357  rdgprc  25423  dfrdg2  25424  dftrpred4g  25513  dfrdg4  25796  colinearalglem4  25849  axlowdimlem3  25884  axlowdimlem16  25897  axlowdimlem17  25898  fvline2  26081  ellines  26087  bpolylem  26095  bpoly1  26098  bpolydiflem  26101  rankeq1o  26113  ordcmp  26198  opnmbllem0  26243  mblfinlem1  26244  mblfinlem2  26245  volsupnfl  26252  ftc1anclem6  26286  ftc1anclem8  26288  ftc2nc  26290  dvreasin  26291  dvreacos  26292  areacirclem1  26293  areacirclem5  26297  clsun  26332  isfne  26349  isref  26360  isptfin  26376  islocfin  26377  neibastop3  26392  cover2g  26417  f1opr  26427  sdclem1  26448  sstotbnd  26485  ssbnd  26498  prdstotbnd  26504  prdsbnd2  26505  ismtyhmeolem  26514  heiborlem3  26523  heiborlem4  26524  heiborlem6  26526  rrnval  26537  rrncmslem  26542  ismrer1  26548  reheibor  26549  rngohomval  26581  rngoisoval  26594  idlval  26624  pridlval  26644  maxidlval  26650  isprrngo  26661  igenval  26672  fndifnfp  26738  elrfi  26749  isnacs  26759  ofmpteq  26777  diophin  26832  dnnumch1  27120  islmodfg  27145  islnm  27153  lnmlssfg  27156  dsmmval  27178  dsmmbas2  27181  dsmmfi  27182  dsmm0cl  27184  frlmpws  27196  frlmlss  27197  frlmbas  27201  uvcfval  27211  frlmsplit2  27221  mapfien2  27236  frlmpwfi  27240  islindf  27260  lindfmm  27275  islindf5  27287  hbtlem1  27305  hbtlem7  27307  hbtlem6  27311  dgrnznn  27318  pmtrmvd  27376  pmtrfrn  27378  psgnunilem2  27396  psgnfval  27401  psgnghm2  27416  mamufval  27421  matval  27443  matplusg2  27455  matvsca2  27456  mdetfval  27465  mendval  27469  mendplusgfval  27471  mendmulrfval  27473  mendvscafval  27476  fgraphxp  27508  iotain  27595  rfcnpre1  27667  rfcnpre2  27679  rfcnpre3  27681  rfcnpre4  27682  fmuldfeq  27690  stoweidlem34  27760  stoweidlem41  27767  stirlinglem7  27806  dfafn5a  28001  dfaimafn2  28007  ffnaov  28040  2wot2wont  28354  2spot2iun2spont  28359  1to2vfriswmgra  28397  usg2spot2nb  28455  dpval  28514  bnj66  29232  bnj570  29277  bnj1326  29396  bnj1463  29425  bnj1501  29437  lshpset  29777  lsatset  29789  lcvfbr  29819  lflset  29858  lkrfval  29886  lkrval2  29889  ldualset  29924  isopos  29979  cmtfvalN  30009  isoml  30037  cvrfval  30067  pats  30084  isatl  30098  iscvlat  30122  ishlat1  30151  llnset  30303  lplnset  30327  lvolset  30370  dalem58  30528  dalem59  30529  lineset  30536  pointsetN  30539  psubspset  30542  pmapfval  30554  paddfval  30595  pclfvalN  30687  polfvalN  30702  psubclsetN  30734  watfvalN  30790  lhpset  30793  lautset  30880  pautsetN  30896  ldilfset  30906  ltrnfset  30915  ltrnset  30916  ltrncoidN  30926  dilfsetN  30950  trnfsetN  30953  trlfset  30958  trlset  30959  cdleme6  31039  cdleme11g  31063  cdleme31sn1  31179  cdleme31sn1c  31186  cdleme31sn2  31187  cdleme40v  31267  cdleme42ke  31283  cdleme50trn2a  31348  cdleme50trn3  31351  cdlemg1b2  31369  cdlemg47  31534  tgrpfset  31542  tgrpset  31543  tendofset  31556  tendoset  31557  erngfset  31597  erngset  31598  erngfset-rN  31605  erngset-rN  31606  cdlemi  31618  cdlemk4  31632  cdlemkuu  31693  cdlemk35  31710  cdlemky  31724  cdlemk54  31756  cdlemk55a  31757  cdlemkyyN  31760  dva1dim  31783  erngdvlem3-rN  31796  dvafset  31802  dvaset  31803  diaffval  31829  diafval  31830  diaintclN  31857  dvhfset  31879  dvhset  31880  cdlemm10N  31917  docaffvalN  31920  docafvalN  31921  djaffvalN  31932  djafvalN  31933  dibffval  31939  dibfval  31940  dib1dim  31964  dibintclN  31966  dicffval  31973  dicfval  31974  dicval2  31978  dihffval  32029  dihfval  32030  dihopelvalcpre  32047  dihmeetbclemN  32103  dih1dimatlem  32128  dihglb2  32141  dihintcl  32143  dochffval  32148  dochfval  32149  djhffval  32195  djhfval  32196  dihjatcclem1  32217  dihjatcclem3  32219  djhlsmat  32226  lpolsetN  32281  lcdfval  32387  lcdval  32388  lcdval2  32389  lcdsca  32398  mapdffval  32425  mapdfval  32426  mapdval3N  32430  mapdval5N  32432  mapdpglem21  32491  hvmapffval  32557  hvmapfval  32558  hdmap1ffval  32595  hdmap1fval  32596  hdmapffval  32628  hdmapfval  32629  hgmapffval  32687  hgmapfval  32688  hdmapoc  32733  hlhilset  32736  hlhilslem  32740  hlhilnvl  32752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2430
  Copyright terms: Public domain W3C validator