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

Theorem syl6eqr 2454
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 2408 . 2  |-  B  =  C
41, 3syl6eq 2452 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  3eqtr4g  2461  iinrab2  4114  relop  4982  dfiun3g  5081  dfiin3g  5082  resima2  5138  relcnvfld  5359  uniabio  5387  iotanul  5392  fntpg  5465  dffn5  5731  dfimafn2  5735  fncnvima2  5811  fmptcof  5861  fcoconst  5864  fnpr  5909  fnprOLD  5910  resfunexg  5916  ffnov  6133  fnov  6137  fnrnov  6178  foov  6179  funimassov  6182  ovelimab  6183  ofc12  6288  caofinvl  6290  1st2val  6331  2nd2val  6332  curry1  6397  curry2  6400  dftpos3  6456  riotav  6513  riotauni  6515  tz7.44-3  6625  rdgsucmptnf  6646  rdglim2a  6650  frsucmptn  6655  seqomlem1  6666  seqomlem4  6669  oa0r  6741  om1r  6745  oarec  6764  oacomf1olem  6766  oeeulem  6803  omabs  6849  ecinxp  6938  mapunen  7235  phplem1  7245  fodomfi  7344  iinfi  7380  fiin  7385  dffi3  7394  ordtypelem3  7445  ordtypelem9  7451  cantnffval  7574  cantnfval  7579  cantnfp1lem3  7592  cantnflem1  7601  wemapwe  7610  oef1o  7611  cnfcom2lem  7614  rankuni  7745  cardval2  7834  dfac8alem  7866  dfac12lem1  7979  cda1dif  8012  cdaassen  8018  isf34lem4  8213  hsmexlem5  8266  axdc3lem4  8289  axdc4lem  8291  ac6num  8315  zorn2lem1  8332  ttukeylem3  8347  pwcfsdom  8414  fpwwe2lem9  8469  canth4  8478  canthp1lem2  8484  genpass  8842  prlem934  8866  mulcmpblnrlem  8904  recexsrlem  8934  supsrlem  8942  axrnegex  8993  nneo  10309  cnref1o  10563  xmulneg1  10804  xmulpnf1n  10813  xadddi  10830  fztp  11058  fseq1m1p1  11078  uzrdgsuci  11255  seqof2  11336  mulexpz  11375  expaddz  11379  bcp1m1  11566  hash1snb  11636  seqcoll  11667  iswrdi  11686  cjexp  11910  rexuz3  12107  limsupval  12223  limsupgle  12226  climconst  12292  zsum  12467  fsum  12469  sum0  12470  sumz  12471  fsumcnv  12512  mertenslem2  12617  efval2  12641  ege2le3  12647  efzval  12658  efival  12708  sinbnd  12736  cosbnd  12737  sadfval  12919  bitsres  12940  smufval  12944  smupp1  12947  eucalgval  13028  eucalginv  13030  eucalglt  13031  eucalgcvga  13032  eucalg  13033  dfphi2  13118  phimullem  13123  prmdiv  13129  odzval  13132  pcval  13173  pczpre  13176  pcrec  13187  prmreclem6  13244  4sqlem17  13284  vdwmc  13301  vdwpc  13303  vdwlem8  13311  ramval  13331  ramcl  13352  ressval  13471  resslem  13477  firest  13615  topnval  13617  prdsval  13633  prdsleval  13654  prdsbas3  13658  prdsdsval2  13661  pwsval  13663  pwsbas  13664  pwselbasb  13665  pwsplusgval  13667  pwsmulrval  13668  pwsle  13669  pwsvscafval  13671  imasval  13692  imasdsval  13696  imasdsval2  13697  divsval  13722  xpsval  13752  xpslem  13753  xpsaddlem  13755  xpsvsca  13759  xpsle  13761  mrisval  13810  iscat  13852  cidfval  13856  homffval  13872  comfffval  13879  comffval  13880  comfeq  13887  oppcval  13894  oppchomfval  13895  oppccofval  13897  oppcid  13902  monfval  13913  oppcmon  13919  sectffval  13931  invffval  13938  isoval  13945  isssc  13975  reschomf  13986  issubc  13990  isfunc  14016  isfuncd  14017  funcf2  14020  idfuval  14028  idfu2nd  14029  cofucl  14040  resfval2  14045  resf2nd  14047  funcres2b  14049  funcpropd  14052  isfull  14062  isfth  14066  natfval  14098  fucval  14110  homafval  14139  homaval  14141  homadmcd  14152  arwval  14153  arwhoma  14155  idafval  14167  coafval  14174  coapm  14181  catcco  14211  catcid  14213  catcisolem  14216  xpcval  14229  xpcco  14235  1stfval  14243  2ndfval  14246  xpcpropd  14260  evlfval  14269  evlfcllem  14273  evlfcl  14274  curfval  14275  curf1cl  14280  curfcl  14284  uncf1  14288  uncf2  14289  uncfcurf  14291  diag2  14297  curf2ndf  14299  hofval  14304  hof2fval  14307  hofcl  14311  yonval  14313  hofpropd  14319  yonedalem21  14325  yonedalem22  14330  yonedalem3  14332  yonedainv  14333  yonffthlem  14334  isdrs  14346  ispos  14359  pltfval  14371  lubfval  14390  glbfval  14395  joinfval  14399  meetfval  14406  p0val  14425  p1val  14426  islat  14431  isclat  14493  ipoval  14535  isipodrs  14542  isdlat  14574  istsr  14604  spwval2  14611  isla  14620  isdir  14632  ismnd  14647  plusffval  14657  grpidval  14662  ismgmid  14665  pws0g  14686  ismhm  14695  submacs  14720  gsumvalx  14729  frmdval  14751  isgrp  14771  grpn0  14792  grpinvfval  14798  grpsubfval  14802  mulgfval  14846  mulgval  14847  mulgnn0p1  14856  pwsinvg  14885  issubg  14899  isnsg  14924  eqgfval  14943  divseccl  14951  isghm  14961  conjsubg  14992  conjsubgen  14993  isgim  15004  isga  15023  symgval  15049  cntrval  15073  cntzfval  15074  oppgval  15098  invoppggim  15111  odfval  15126  odval  15127  gexval  15167  ispgp  15181  sylow1lem1  15187  slwispgp  15200  pgpssslw  15203  sylow2alem2  15207  sylow3lem5  15220  lsmfval  15227  pj1fval  15281  efgmnvl  15301  efgval  15304  efgval2  15311  efginvrel2  15314  efgsfo  15326  efgredleme  15330  efgredlemd  15331  efgredlemc  15332  frgpval  15345  frgpeccl  15348  vrgpfval  15353  frgpuptinv  15358  frgpup3lem  15364  iscmn  15374  subcmn  15411  frgpnabllem1  15439  iscyg  15444  lt6abl  15459  gsumval3  15469  gsumzf1o  15474  gsum2d  15501  gsumcom2  15504  dmdprd  15514  dprdval  15516  dprd2da  15555  dmdprdsplit2lem  15558  dpjfval  15568  pgpfaclem1  15594  mgpval  15606  mgpplusg  15607  isrng  15623  iscrng  15626  pws1  15677  opprval  15684  crngoppr  15687  dvdsrval  15705  isunit  15717  invrfval  15733  dvrfval  15744  isirred  15759  dfrhm2  15776  pwsco1rhm  15788  pwsco2rhm  15789  isdrng  15794  isdrng2  15800  drngid  15804  isdrngrd  15816  issubrg  15823  abvfval  15861  abvneg  15877  staffval  15890  issrng  15893  issrngd  15904  islmod  15909  scaffval  15923  lssset  15965  prdsvscacl  15999  lspfval  16004  islmhm  16058  islmhm2  16069  islmim  16089  islbs  16103  islvec  16131  2idlval  16259  crng2idl  16265  isnzr  16285  rrgval  16302  isdomn  16309  isassa  16330  aspval  16342  asclfval  16348  psrval  16384  mvrfval  16439  mplval  16447  mplcoe3  16484  mplcoe2  16485  ltbval  16487  opsrval  16490  mplind  16517  vr1cl2  16546  ply1val  16547  psropprmul  16587  coe1mul2lem2  16616  coe1tm  16620  coe1sclmul  16629  coe1sclmul2  16631  ply1scl1  16638  ply1coe  16639  mulgrhm2  16743  zlmval  16752  chrval  16761  znval  16771  znzrhfo  16783  znle2  16789  znunithash  16800  cygznlem1  16802  isphl  16814  phllmhm  16818  ipffval  16834  ocvfval  16848  cssval  16864  cssincl  16870  thlval  16877  pjfval  16888  ishil  16900  isobs  16902  istps  16956  cldval  17042  ntrfval  17043  clsfval  17044  neifval  17118  lpfval  17157  isperf  17169  restbas  17176  tgrest  17177  resstopn  17204  ordtval  17207  ordtuni  17208  ordtbas  17210  ordtrest2  17222  ist0  17338  ist1  17339  ishaus  17340  iscnrm  17341  pnrmopn  17361  iscmp  17405  cmpcld  17419  hauscmplem  17423  cmpfi  17425  iscon  17429  consuba  17436  is1stc  17457  txval  17549  ptval  17555  ptbasin  17562  ptbasfi  17566  xkoval  17572  ptunimpt  17580  ptval2  17586  txbasval  17591  dfac14  17603  upxp  17608  uptx  17610  prdstopn  17613  txrest  17616  ptrescn  17624  lmcn2  17634  xkoptsub  17639  xkopt  17640  xkococn  17645  cnmpt2t  17658  cnmpt2res  17662  cnmpt2k  17673  imasnopn  17675  imasncld  17676  imasncls  17677  qtopval  17680  imastopn  17705  hmphindis  17782  ptuncnv  17792  ptunhmeo  17793  xpstopnlem1  17794  xpstopnlem2  17796  xkohmeo  17800  qtophmeo  17802  elmptrab  17812  trfbas2  17828  trfil2  17872  fmco  17946  flimval  17948  flfcnp2  17992  fclsval  17993  fclsrest  18009  alexsublem  18028  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem1  18036  ptcmplem3  18038  ptcmpg  18041  istmd  18057  istgp  18060  istgp2  18074  tgplacthmeo  18086  clssubg  18091  tgpconcompeqg  18094  tsmsval2  18112  istrg  18146  istdrg  18148  istlm  18167  istvc  18174  ustbas  18210  trust  18212  ustuqtop1  18224  ustuqtop2  18225  utopsnneiplem  18230  utop2nei  18233  utop3cls  18234  utopreg  18235  isusp  18244  psmetxrge0  18297  imasdsf1olem  18356  xpsxmetlem  18362  xpsmet  18365  isxms  18430  isms  18432  tmsval  18464  stdbdxmet  18498  prdsxmslem2  18512  txmetcnp  18530  nmfval  18589  isngp  18596  tngval  18633  tngtopn  18644  tngnm  18645  isnrg  18649  isnlm  18664  nmofval  18701  nghmfval  18709  qtopbaslem  18745  cnblcld  18762  negcncf  18901  negfcncf  18902  cncfcnvcn  18904  cnmptre  18905  cnheiborlem  18932  cnheibor  18933  bndth  18936  pcorev2  19006  om1bas  19009  pi1val  19015  pi1bas3  19021  pi1cpbl  19022  pi1xfrcnv  19035  isclm  19042  nmoleub2lem3  19076  nmoleub3  19080  iscph  19086  cphcjcl  19099  tchval  19130  ipcau2  19144  csscld  19156  iscmet  19190  caubl  19213  caublcls  19214  bcthlem4  19233  bcthlem5  19234  bcth3  19237  isbn  19244  iscms  19251  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovolfsval  19320  ovolval  19323  ovollb2lem  19337  ovolctb  19339  ovolunlem1a  19345  ovoliunlem1  19351  ovoliun2  19355  shft2rab  19357  ovolshftlem1  19358  sca2rab  19361  ovolscalem1  19362  ovolicc2lem1  19366  ovolicc2lem4  19369  ovolicc2lem5  19370  cmmbl  19382  unmbl  19385  voliunlem3  19399  iunmbl  19400  voliun  19401  ioombl1lem3  19407  ovolfs2  19416  ioorinv  19421  uniiccdif  19423  uniioovol  19424  uniioombllem2a  19427  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombllem6  19433  dyadovol  19438  dyadss  19439  dyaddisjlem  19440  dyadmaxlem  19442  dyadmbl  19445  opnmbllem  19446  vitalilem4  19456  ismbf  19475  mbfconst  19480  itg2val  19573  itg2monolem1  19595  itg2i1fseq  19600  dfitg  19614  itgz  19625  itgvallem3  19630  iblcnlem1  19632  iblcnlem  19633  iblposlem  19636  itgreval  19641  itgfsum  19671  bddmulibl  19683  itgcn  19687  limcfval  19712  ellimc  19713  limcmpt2  19724  limccnp  19731  dvfval  19737  eldv  19738  dvreslem  19749  dvres2lem  19750  dvidlem  19755  dvnfval  19761  dvexp2  19793  dvrec  19794  dveflem  19816  dvlipcn  19831  dv11cn  19838  lhop  19853  ftc2  19881  evlsval  19893  evlsval2  19894  evlval  19898  evlrhm  19899  evl1fval  19900  evl1sca  19903  evl1var  19905  pf1subrg  19921  pf1ind  19928  mdegfval  19938  uc1pval  20015  mon1pval  20017  q1pval  20029  r1pval  20032  ig1pval  20048  plyconst  20078  plyeq0lem  20082  dgrval  20100  plyco  20113  0dgrb  20118  coemullem  20121  coe0  20127  coesub  20128  dgrsub  20143  dgrcolem1  20144  dgrcolem2  20145  dgrco  20146  quotval  20162  plydivex  20167  quotlem  20170  plyremlem  20174  fta1  20178  vieta1lem1  20180  vieta1lem2  20181  vieta1  20182  aaliou2  20210  aaliou3lem7  20219  taylpfval  20234  dvtaylp  20239  dvntaylp0  20241  taylthlem1  20242  ulm2  20254  ulmshft  20259  pserdvlem2  20297  abelthlem1  20300  abelthlem8  20308  abelth  20310  abelth2  20311  ptolemy  20357  coskpi  20381  efif1olem2  20398  efif1olem3  20399  logcnlem4  20489  advlogexp  20499  efopn  20502  logtayl  20504  dcubic2  20637  dcubic  20639  quart1lem  20648  atancj  20703  tanatan  20712  cosatan  20714  dvatan  20728  leibpi  20735  birthdaylem2  20744  efrlim  20761  emcllem7  20793  wilthlem2  20805  basellem5  20820  basellem8  20823  basellem9  20824  vmaval  20849  prmorcht  20914  mumul  20917  dvdsmulf1o  20932  fsumdvdsmul  20933  ppiub  20941  fsumvma  20950  pclogsum  20952  dchrval  20971  bposlem8  21028  lgslem1  21033  lgsval  21037  lgsval4  21053  lgsfcl3  21054  lgsdilem  21059  lgsdir2lem4  21063  lgsdir2lem5  21064  lgsquadlem2  21092  dchrisum0flb  21157  rpvmasum2  21159  log2sumbnd  21191  selberglem2  21193  pntibndlem2  21238  pntlemp  21257  ostth2lem3  21282  ostth2lem4  21283  umgraex  21311  usgraexvlem  21367  nbgraf1olem5  21408  constr3trllem3  21592  constr3cycllem1  21598  vdgr1d  21627  eupath2lem3  21654  isplig  21718  gidval  21754  grpoinvfval  21765  grpodivfval  21783  gxfval  21798  isablo  21824  subgornss  21847  isexid  21858  elghomlem1  21902  isrngo  21919  drngoi  21948  vci  21980  isvclem  22009  nvop2  22040  nvvop  22041  isnvlem  22042  dipfval  22151  sspval  22175  isssp  22176  lnoval  22206  nmoofval  22216  bloval  22235  0ofval  22241  ajfval  22263  hmoval  22264  isphg  22271  phop  22272  ipasslem11  22294  siii  22307  iscbn  22319  opsqrlem6  23601  elpjrn  23646  hstle1  23682  stm1addi  23701  stm1add3i  23703  mdslmd1lem1  23781  mdexchi  23791  atordi  23840  dmdbr5ati  23878  cdj3lem1  23890  disjabrex  23977  disjabrexf  23978  csbcnvg  23990  feqmptdf  24028  xrofsup  24079  isofld  24188  subofld  24198  inftmrel  24203  isinftm  24204  pstmfval  24244  xpinpreima2  24258  zlmds  24301  qqhval  24311  rrhval  24332  xrhval  24337  esumsn  24409  ofcc  24442  sxval  24497  measvuni  24521  volmeas  24540  elunirnmbfm  24556  sitgval  24600  sibfof  24607  sitgclcn  24611  sitgclre  24612  totprob  24638  orrvcval4  24675  lgamcvglem  24777  subfacp1lem5  24823  subfacp1lem6  24824  ispcon  24863  pconpi1  24877  rescon  24886  iscvm  24899  cvmsss2  24914  cvmliftlem3  24927  cvmliftlem5  24929  cvmliftlem10  24934  cvmliftlem11  24935  cvmlift2lem9a  24943  cvmlift2lem2  24944  cvmliftphtlem  24957  cvmlift3lem7  24965  snmlflim  24972  ghomgrpilem2  25050  fz0n  25155  zprod  25216  fprod  25220  prod0  25222  prod1  25223  fprodcnv  25260  fallfacfwd  25303  binomfallfaclem2  25307  rdgprc  25365  dfrdg2  25366  dftrpred4g  25451  dfrdg4  25703  colinearalglem4  25752  axlowdimlem3  25787  axlowdimlem16  25800  axlowdimlem17  25801  fvline2  25984  ellines  25990  bpolylem  25998  bpoly1  26001  bpolydiflem  26004  rankeq1o  26016  ordcmp  26101  mblfinlem  26143  volsupnfl  26150  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem6  26186  clsun  26221  isfne  26238  isref  26249  isptfin  26265  islocfin  26266  neibastop3  26281  cover2g  26306  f1opr  26316  sdclem1  26337  sstotbnd  26374  ssbnd  26387  prdstotbnd  26393  prdsbnd2  26394  ismtyhmeolem  26403  heiborlem3  26412  heiborlem4  26413  heiborlem6  26415  rrnval  26426  rrncmslem  26431  ismrer1  26437  reheibor  26438  rngohomval  26470  rngoisoval  26483  idlval  26513  pridlval  26533  maxidlval  26539  isprrngo  26550  igenval  26561  fndifnfp  26627  elrfi  26638  isnacs  26648  ofmpteq  26666  diophin  26721  dnnumch1  27009  islmodfg  27035  islnm  27043  lnmlssfg  27046  dsmmval  27068  dsmmbas2  27071  dsmmfi  27072  dsmm0cl  27074  frlmpws  27086  frlmlss  27087  frlmbas  27091  uvcfval  27101  frlmsplit2  27111  mapfien2  27126  frlmpwfi  27130  islindf  27150  lindfmm  27165  islindf5  27177  hbtlem1  27195  hbtlem7  27197  hbtlem6  27201  dgrnznn  27208  pmtrmvd  27266  pmtrfrn  27268  psgnunilem2  27286  psgnfval  27291  psgnghm2  27306  mamufval  27311  matval  27333  matplusg2  27345  matvsca2  27346  mdetfval  27355  mendval  27359  mendplusgfval  27361  mendmulrfval  27363  mendvscafval  27366  fgraphxp  27398  iotain  27485  rfcnpre1  27557  rfcnpre2  27569  rfcnpre3  27571  rfcnpre4  27572  fmuldfeq  27580  stoweidlem34  27650  stoweidlem41  27657  stirlinglem7  27696  dfafn5a  27891  dfaimafn2  27897  ffnaov  27930  2wot2wont  28083  2spot2iun2spont  28088  1to2vfriswmgra  28110  usg2spot2nb  28168  dpval  28227  bnj66  28937  bnj570  28982  bnj1326  29101  bnj1463  29130  bnj1501  29142  lshpset  29461  lsatset  29473  lcvfbr  29503  lflset  29542  lkrfval  29570  lkrval2  29573  ldualset  29608  isopos  29663  cmtfvalN  29693  isoml  29721  cvrfval  29751  pats  29768  isatl  29782  iscvlat  29806  ishlat1  29835  llnset  29987  lplnset  30011  lvolset  30054  dalem58  30212  dalem59  30213  lineset  30220  pointsetN  30223  psubspset  30226  pmapfval  30238  paddfval  30279  pclfvalN  30371  polfvalN  30386  psubclsetN  30418  watfvalN  30474  lhpset  30477  lautset  30564  pautsetN  30580  ldilfset  30590  ltrnfset  30599  ltrnset  30600  ltrncoidN  30610  dilfsetN  30634  trnfsetN  30637  trlfset  30642  trlset  30643  cdleme6  30723  cdleme11g  30747  cdleme31sn1  30863  cdleme31sn1c  30870  cdleme31sn2  30871  cdleme40v  30951  cdleme42ke  30967  cdleme50trn2a  31032  cdleme50trn3  31035  cdlemg1b2  31053  cdlemg47  31218  tgrpfset  31226  tgrpset  31227  tendofset  31240  tendoset  31241  erngfset  31281  erngset  31282  erngfset-rN  31289  erngset-rN  31290  cdlemi  31302  cdlemk4  31316  cdlemkuu  31377  cdlemk35  31394  cdlemky  31408  cdlemk54  31440  cdlemk55a  31441  cdlemkyyN  31444  dva1dim  31467  erngdvlem3-rN  31480  dvafset  31486  dvaset  31487  diaffval  31513  diafval  31514  diaintclN  31541  dvhfset  31563  dvhset  31564  cdlemm10N  31601  docaffvalN  31604  docafvalN  31605  djaffvalN  31616  djafvalN  31617  dibffval  31623  dibfval  31624  dib1dim  31648  dibintclN  31650  dicffval  31657  dicfval  31658  dicval2  31662  dihffval  31713  dihfval  31714  dihopelvalcpre  31731  dihmeetbclemN  31787  dih1dimatlem  31812  dihglb2  31825  dihintcl  31827  dochffval  31832  dochfval  31833  djhffval  31879  djhfval  31880  dihjatcclem1  31901  dihjatcclem3  31903  djhlsmat  31910  lpolsetN  31965  lcdfval  32071  lcdval  32072  lcdval2  32073  lcdsca  32082  mapdffval  32109  mapdfval  32110  mapdval3N  32114  mapdval5N  32116  mapdpglem21  32175  hvmapffval  32241  hvmapfval  32242  hdmap1ffval  32279  hdmap1fval  32280  hdmapffval  32312  hdmapfval  32313  hgmapffval  32371  hgmapfval  32372  hdmapoc  32417  hlhilset  32420  hlhilslem  32424  hlhilnvl  32436
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 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator