Theorem eqtr2d 2779

Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)

Hypotheses

Ref	Expression
eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr2d.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtr2d	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2d

Step	Hyp	Ref	Expression
1		eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	eqtrd 2778	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2744	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  3eqtrrd  2783  3eqtr2rd  2785  ifan  4509  ifor  4510  dfopifOLD  4798  fnco  6533  fnsnfv  6829  nvocnv  7134  elovmpt3rab1  7507  onsucmin  7643  csbopeq1a  7864  oaabs2  8439  ecinxp  8539  fsetfocdm  8607  resixpfo  8682  sbthlem3  8825  rankxpsuc  9571  fseqenlem2  9712  dfac2b  9817  isf32lem9  10048  compsscnvlem  10057  ttukeylem7  10202  fpwwe2lem10  10327  00id  11080  submul2  11345  mulsubfacd  11366  divadddiv  11620  infrenegsup  11888  xadd4d  12966  fzdifsuc  13245  fzval3  13384  fzoshftral  13432  ceim1l  13495  fldiv  13508  flmod  13533  intfrac  13534  modcyc2  13555  moddi  13587  uzrdgfni  13606  axdc4uzlem  13631  seqf1olem1  13690  seqf1olem2  13691  seqid2  13697  expnegz  13745  binom2sub  13863  binom3  13867  hashreshashfun  14082  ccatw2s1p2  14276  ccats1pfxeq  14355  pfxccatin12lem2  14372  pfxccatin12  14374  swrdccat3b  14381  cshweqrep  14462  2cshwcshw  14466  ccatco  14476  swrds2  14581  relexpsucnnr  14664  relexpaddnn  14690  reim  14748  mulre  14760  addcj  14787  absimle  14949  clim2ser  15294  isercoll2  15308  serf0  15320  iseralt  15324  summolem3  15354  isumclim3  15399  mptfzshft  15418  fsumrev  15419  fsum2mul  15429  incexc  15477  isumsplit  15480  mertenslem1  15524  fprodrev  15615  iprodclim3  15638  binomfallfaclem2  15678  ef4p  15750  tanval3  15771  efival  15789  sinmul  15809  bitsinvp1  16084  sadaddlem  16101  bitsshft  16110  smu01lem  16120  dfgcd2  16182  lcmgcdlem  16239  lcm1  16243  lcmfass  16279  eulerthlem2  16411  hashgcdeq  16418  powm2modprm  16432  pythagtriplem16  16459  pczpre  16476  pcqdiv  16486  pcadd  16518  pcfac  16528  prmreclem5  16549  4sqlem10  16576  4sqlem19  16592  vdwapun  16603  vdwlem1  16610  ramcl  16658  setsstruct  16805  strfvd  16830  strfv2d  16831  xpsff1o  17195  xpsrnbas  17199  2oppccomf  17353  oppcepi  17368  sscfn1  17446  sscfn2  17447  invfuc  17608  funcestrcsetclem7  17779  funcsetcestrclem7  17794  gsumsplit1r  18286  grpinvssd  18567  grpinvval2  18573  cycsubggend  18739  pmtrdifwrdellem2  19005  psgnunilem1  19016  psgnuni  19022  pgp0  19116  sylow1lem1  19118  sylow3lem2  19148  efgredleme  19264  efgcpbllemb  19276  frgpuptinv  19292  frgpup3lem  19298  gexexlem  19368  cyggenod  19399  gsumval3eu  19420  gsumval3  19423  gsumzaddlem  19437  dprd2db  19561  ablsimpgfindlem1  19625  ringinvdv  19851  lss1d  20140  pwssplit1  20236  znzrh2  20665  regsumsupp  20739  ipassr2  20764  dsmmfi  20855  frlmlss  20868  frlmip  20895  frlmlbs  20914  frlmup3  20917  islindf4  20955  mplcoe3  21149  subrgascl  21184  evlseu  21203  ply1sclid  21369  1marepvmarrepid  21632  madurid  21701  smadiadetlem3  21725  mat2pmatghm  21787  pmatcollpwscmatlem1  21846  pm2mpmhmlem2  21876  cpmadurid  21924  cpmidgsumm2pm  21926  cpmadugsumlemB  21931  cayhamlem2  21941  ntrval2  22110  ordtuni  22249  cnclima  22327  cmpsub  22459  ptbasfi  22640  txbasval  22665  pt1hmeo  22865  alexsubALTlem1  23106  trust  23289  ussid  23320  ressuss  23322  ressprdsds  23432  imasdsf1olem  23434  setsms  23541  tmsxms  23548  tmsxpsmopn  23599  subgnm  23695  tngnm  23721  tngngp2  23722  xrsxmet  23878  xrge0gsumle  23902  metdstri  23920  xrhmeo  24015  lebnumlem3  24032  pcorevlem  24095  pi1xfrcnvlem  24125  clmabs  24152  cvsmuleqdivd  24203  rrxip  24459  rrxds  24462  rrxdsfi  24480  minveclem4a  24499  pjthlem1  24506  divcncf  24516  ovolunlem1a  24565  mbfres2  24714  i1faddlem  24762  ibladdlem  24889  iblabs  24898  ditgsplit  24930  dvmptresicc  24985  dvnres  25000  dvmptdiv  25043  dveflem  25048  dveq0  25069  dvfsumabs  25092  itgsubstlem  25117  ply1divex  25206  dgrco  25341  plycjlem  25342  taylthlem1  25437  pserdv2  25494  abelthlem6  25500  abelthlem7  25502  tangtx  25567  abssinper  25582  sineq0  25585  explog  25654  reexplog  25655  eflogeq  25662  abslogle  25678  tanarg  25679  logtayl  25720  logtayl2  25722  relogbdiv  25834  ang180lem3  25866  affineequiv  25878  affineequiv2  25879  chordthmlem4  25890  chordthmlem5  25891  heron  25893  dcubic1lem  25898  dcubic2  25899  dcubic  25901  mcubic  25902  cubic2  25903  dquartlem1  25906  dquart  25908  quart1lem  25910  quartlem1  25912  quart  25916  acoscos  25948  atanlogaddlem  25968  atantayl2  25993  atantayl3  25994  birthdaylem2  26007  efrlim  26024  amgmlem  26044  logdifbnd  26048  emcllem3  26052  emcllem6  26055  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  gamigam  26107  lgamcvg2  26109  gamfac  26121  basellem3  26137  basellem8  26142  basellem9  26143  chtprm  26207  logfaclbnd  26275  perfect1  26281  bcp1ctr  26332  bclbnd  26333  bposlem1  26337  lgsdilem  26377  lgsdirnn0  26397  lgsdinn0  26398  gausslemma2dlem1a  26418  gausslemma2dlem4  26422  gausslemma2dlem5a  26423  lgseisenlem2  26429  lgsquadlem1  26433  2sqlem2  26471  mul2sq  26472  2sqmod  26489  2sqnn0  26491  vmadivsum  26535  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasum2if  26550  dchrisum0lem2  26571  logsqvma2  26596  selberg3  26612  selberg4lem1  26613  pntrsumo1  26618  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntibndlem2  26644  pntlemk  26659  pntlemo  26660  ostth2lem4  26689  ostth3  26691  tgbtwndiff  26771  tgifscgr  26773  trgcgrg  26780  motcgr3  26810  tgbtwnconn1lem1  26837  tgbtwnconn1lem2  26838  ismir  26924  miriso  26935  midexlem  26957  ragmir  26965  footexALT  26983  footexlem1  26984  footexlem2  26985  colperpexlem3  26997  mideulem2  26999  midex  27002  opphllem3  27014  midcgr  27045  lmiisolem  27061  brbtwn2  27176  colinearalglem4  27180  axsegconlem1  27188  axpaschlem  27211  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  ushgredgedgloop  27501  crctcshwlkn0lem6  28081  wwlknlsw  28113  wwlksnextwrd  28163  clwlkclwwlklem2a3  28259  clwlkclwwlk2  28268  clwwlkel  28311  clwwlkfo  28315  clwwlkext2edg  28321  eupth2eucrct  28482  numclwwlk2lem1lem  28607  numclwwlk1lem2fo  28623  numclwlk2lem2f  28642  grpoidinvlem2  28768  nvmtri  28934  cnnvm  28945  nvnd  28951  ipidsq  28973  ipnm  28974  ipipcj  28978  blocnilem  29067  ipasslem2  29095  dipsubdir  29111  hvaddsubval  29296  pjhthlem1  29654  pjspansn  29840  pjo  29934  unoplin  30183  adjadj  30199  hmoplin  30205  eigvec1  30225  lnopeqi  30271  nmcexi  30289  lnfnsubi  30309  riesz3i  30325  kbass6  30384  leoprf2  30390  leoprf  30391  pjnmopi  30411  mdslmd1lem1  30588  mdslmd1lem2  30589  superpos  30617  ifeq3da  30790  fgreu  30911  resf1o  30967  fprodex01  31041  wrdt2ind  31127  gsummpt2d  31211  xrge0tsmseq  31221  symgfcoeu  31253  psgnfzto1stlem  31269  psgnfzto1st  31274  cycpm2tr  31288  cycpmco2lem6  31300  cycpmco2lem7  31301  subrgchr  31393  rhmdvd  31422  nsgqusf1olem3  31502  ply1chr  31571  dimval  31588  dimvalfi  31589  lindsunlem  31607  dimkerim  31610  qusdimsum  31611  fedgmullem1  31612  extdg1id  31640  madjusmdetlem2  31680  qtophaus  31688  zarclssn  31725  zarcmplem  31733  pstmval  31747  mndpluscn  31778  qqhucn  31842  esumval  31914  gsumesum  31927  esumcst  31931  esumpcvgval  31946  oddpwdc  32221  eulerpartlemgvv  32243  probdif  32287  sgnmul  32409  signsvtn  32463  actfunsnf1o  32484  reprpmtf1o  32506  hgt750lemd  32528  logdivsqrle  32530  hgt750lemg  32534  hgt750lemb  32536  bnj1415  32918  swrdrevpfx  32978  pfxwlk  32985  derangen2  33036  subfaclefac  33038  subfaclim  33050  satom  33218  fmla  33243  mrsubrn  33375  sinccvglem  33530  bcprod  33610  filnetlem4  34497  curunc  35686  ltflcei  35692  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  mblfinlem4  35744  ibladdnclem  35760  iblabsnc  35768  iblmulc2nc  35769  ftc1anclem6  35782  ftc1anclem8  35784  sdclem2  35827  ismtycnv  35887  heiborlem10  35905  lflvsass  37022  lkrscss  37039  eqlkr  37040  eqlkr3  37042  ldualvsdi2  37085  omllaw3  37186  cmtcomlemN  37189  cmtbr3N  37195  omlfh3N  37200  llnexchb2lem  37809  dalawlem7  37818  dalawlem11  37822  dalawlem12  37823  pol1N  37851  paddatclN  37890  4atexlemcnd  38013  ltrncoidN  38069  cdleme3b  38170  cdleme11  38211  cdleme15a  38215  cdleme22e  38285  cdleme22g  38289  cdlemg18b  38620  trlcoat  38664  cdlemk2  38773  cdlemk4  38775  cdlemki  38782  cdlemksv2  38788  cdlemk15  38796  cdlemk55a  38900  diainN  38998  dia2dimlem3  39007  dia2dimlem5  39009  dvhlveclem  39049  diaocN  39066  cdlemn4  39139  cdlemn8  39145  dihopelvalcpre  39189  dihmeetlem9N  39256  dih1dimatlem  39270  dihpN  39277  dochvalr3  39304  dochsat  39324  djhjlj  39344  dochdmm1  39351  dihjatcclem4  39362  dihjat1  39370  dihjat4  39374  dochsnkr2cl  39415  dochfl1  39417  lclkrlem2j  39457  mapdordlem2  39578  mapdrvallem2  39586  hdmap10  39781  lcmineqlem12  39976  3lexlogpow5ineq5  39996  aks4d1p1  40012  frlmvscadiccat  40163  frlmsnic  40188  fsuppind  40202  cnreeu  40359  flt4lem7  40412  negexpidd  40420  3cubeslem2  40423  3cubeslem3r  40425  mzpsubmpt  40481  irrapxlem3  40562  pellexlem6  40572  pell1234qrne0  40591  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell14qrdich  40607  pell1qrgaplem  40611  rmxluc  40674  rmyluc  40675  jm2.24nn  40697  jm2.18  40726  jm2.19lem2  40728  jm2.19lem3  40729  jm2.22  40733  jm2.23  40734  jm2.16nn0  40742  jm2.27c  40745  fnwe2lem2  40792  lmhmfgsplit  40827  hbtlem2  40865  reabssgn  41133  relexpmulnn  41206  relexpmulg  41207  ntrclsneine0lem  41563  int-addassocd  41674  dvconstbi  41841  bccm1k  41849  binomcxplemnotnn0  41863  fmptsnxp  42594  wessf1ornlem  42611  projf1o  42625  infnsuprnmpt  42685  lefldiveq  42721  lt4addmuld  42735  fzdifsuc2  42739  suplesup  42768  infrpge  42780  xrlexaddrp  42781  xralrple2  42783  infleinflem1  42799  supminfrnmpt  42875  supminfxr2  42899  fsumnncl  43003  limcperiod  43059  sumnnodd  43061  limcresiooub  43073  limcresioolb  43074  0ellimcdiv  43080  reclimc  43084  limsupval3  43123  limsupequzmpt2  43149  liminfval5  43196  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  liminfequzmpt2  43222  climliminflimsupd  43232  liminfltlem  43235  liminflbuz2  43246  sinmulcos  43296  coskpi2  43297  cncfdmsn  43321  cncfiooicclem1  43324  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  fperdvper  43350  dvnmptdivc  43369  dvnxpaek  43373  dvnmul  43374  dvnprodlem1  43377  dvnprodlem3  43379  itgcoscmulx  43400  itgsincmulx  43405  itgspltprt  43410  itgiccshift  43411  itgperiod  43412  sublevolico  43415  volioof  43418  ovolsplit  43419  fvvolioof  43420  fvvolicof  43422  stoweidlem22  43453  stoweidlem32  43463  wallispilem5  43500  stirlinglem5  43509  dirkertrigeqlem2  43530  dirkertrigeq  43532  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem13  43551  fourierdlem16  43554  fourierdlem19  43557  fourierdlem21  43559  fourierdlem22  43560  fourierdlem28  43566  fourierdlem32  43570  fourierdlem33  43571  fourierdlem42  43580  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem56  43593  fourierdlem60  43597  fourierdlem61  43598  fourierdlem64  43601  fourierdlem66  43603  fourierdlem71  43608  fourierdlem73  43610  fourierdlem74  43611  fourierdlem76  43613  fourierdlem78  43615  fourierdlem79  43616  fourierdlem80  43617  fourierdlem81  43618  fourierdlem83  43620  fourierdlem88  43625  fourierdlem92  43629  fourierdlem93  43630  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem109  43646  fourierdlem111  43648  fouriersw  43662  elaa2lem  43664  etransclem24  43689  etransclem25  43690  etransclem35  43700  etransclem46  43711  rrndistlt  43721  rrxunitopnfi  43723  qndenserrnbl  43726  qndenserrnopnlem  43728  saldifcl2  43757  intsal  43759  sge0sn  43807  sge0ltfirp  43828  sge0iunmptlemre  43843  sge0fodjrnlem  43844  sge0isum  43855  sge0xaddlem1  43861  nnfoctbdjlem  43883  meassle  43891  ismeannd  43895  meadif  43907  meaiuninclem  43908  meaiininclem  43914  omeunile  43933  caragendifcl  43942  caratheodory  43956  isomenndlem  43958  ovnsubaddlem1  43998  hoidmv1lelem2  44020  hoidmv1le  44022  hoidmvlelem2  44024  hoidmvle  44028  hoi2toco  44035  rrnmbl  44042  hoidifhspdmvle  44048  voncmpl  44049  hoiqssbl  44053  hspmbllem1  44054  hspmbllem2  44055  ovolval2lem  44071  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  hoimbl2  44093  vonhoire  44100  salpreimagelt  44132  salpreimalegt  44134  preimaioomnf  44143  smfres  44211  smfmullem1  44212  smflimmpt  44230  smfsupmpt  44235  smfinfmpt  44239  smflimsupmpt  44249  smfliminflem  44250  smfliminfmpt  44252  sigarcol  44267  f1oresf1o  44669  elsprel  44815  prproropf1o  44847  paireqne  44851  sfprmdvdsmersenne  44943  lighneallem3  44947  lighneallem4  44950  nn0onn0exALTV  45039  nnsum3primesprm  45130  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  c0snmgmhm  45360  rngcifuestrc  45443  funcrngcsetc  45444  funcrngcsetcALT  45445  funcringcsetc  45481  funcringcsetcALTV2lem7  45488  funcringcsetclem7ALTV  45511  lincext3  45685  lincresunit3  45710  nn0onn0ex  45757  nnpw2pmod  45817  blennn0em1  45825  digexp  45841  dignn0ehalf  45851  nn0mulfsum  45858  itcovalpclem1  45904  eenglngeehlnmlem2  45972  rrx2vlinest  45975  line2  45986  itschlc0xyqsol  46001  itsclinecirc0b  46008  toplatjoin  46176  toplatmeet  46177  recsec  46344  reccsc  46345  aacllem  46391  amgmlemALT  46393