Theorem eqtr2d 2774

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 2773	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2739	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  3eqtrrd  2778  3eqtr2rd  2780  ifan  4582  ifor  4583  dfopif  4871  fnco  6668  fnsnfv  6971  nvocnv  7279  elovmpt3rab1  7666  onsucmin  7809  csbopeq1a  8036  oaabs2  8648  ecinxp  8786  fsetfocdm  8855  resixpfo  8930  sbthlem3  9085  rankxpsuc  9877  fseqenlem2  10020  dfac2b  10125  isf32lem9  10356  compsscnvlem  10365  ttukeylem7  10510  fpwwe2lem10  10635  00id  11389  submul2  11654  mulsubfacd  11675  divadddiv  11929  infrenegsup  12197  xadd4d  13282  fzdifsuc  13561  fzval3  13701  fzoshftral  13749  ceim1l  13812  fldiv  13825  flmod  13850  intfrac  13851  modcyc2  13872  moddi  13904  uzrdgfni  13923  axdc4uzlem  13948  seqf1olem1  14007  seqf1olem2  14008  seqid2  14014  expnegz  14062  binom2sub  14183  binom3  14187  hashreshashfun  14399  ccatw2s1p2  14587  ccats1pfxeq  14664  pfxccatin12lem2  14681  pfxccatin12  14683  swrdccat3b  14690  cshweqrep  14771  2cshwcshw  14776  ccatco  14786  swrds2  14891  relexpsucnnr  14972  relexpaddnn  14998  reim  15056  mulre  15068  addcj  15095  absimle  15256  clim2ser  15601  isercoll2  15615  serf0  15627  iseralt  15631  summolem3  15660  isumclim3  15705  mptfzshft  15724  fsumrev  15725  fsum2mul  15735  incexc  15783  isumsplit  15786  mertenslem1  15830  fprodrev  15921  iprodclim3  15944  binomfallfaclem2  15984  ef4p  16056  tanval3  16077  efival  16095  sinmul  16115  bitsinvp1  16390  sadaddlem  16407  bitsshft  16416  smu01lem  16426  dfgcd2  16488  lcmgcdlem  16543  lcm1  16547  lcmfass  16583  eulerthlem2  16715  hashgcdeq  16722  powm2modprm  16736  pythagtriplem16  16763  pczpre  16780  pcqdiv  16790  pcadd  16822  pcfac  16832  prmreclem5  16853  4sqlem10  16880  4sqlem19  16896  vdwapun  16907  vdwlem1  16914  ramcl  16962  setsstruct  17109  strfvd  17134  strfv2d  17135  xpsff1o  17513  xpsrnbas  17517  2oppccomf  17671  oppcepi  17686  sscfn1  17764  sscfn2  17765  invfuc  17927  funcestrcsetclem7  18098  funcsetcestrclem7  18113  gsumsplit1r  18606  grpinvssd  18900  grpinvval2  18906  cycsubggend  19082  pmtrdifwrdellem2  19350  psgnunilem1  19361  psgnuni  19367  pgp0  19464  sylow1lem1  19466  sylow3lem2  19496  efgredleme  19611  efgcpbllemb  19623  frgpuptinv  19639  frgpup3lem  19645  gexexlem  19720  cyggenod  19752  gsumval3eu  19772  gsumval3  19775  gsumzaddlem  19789  dprd2db  19913  ablsimpgfindlem1  19977  ringinvdv  20228  lss1d  20574  pwssplit1  20670  znzrh2  21101  regsumsupp  21175  ipassr2  21200  dsmmfi  21293  frlmlss  21306  frlmip  21333  frlmlbs  21352  frlmup3  21355  islindf4  21393  mplcoe3  21593  subrgascl  21627  evlseu  21646  ply1sclid  21810  1marepvmarrepid  22077  madurid  22146  smadiadetlem3  22170  mat2pmatghm  22232  pmatcollpwscmatlem1  22291  pm2mpmhmlem2  22321  cpmadurid  22369  cpmidgsumm2pm  22371  cpmadugsumlemB  22376  cayhamlem2  22386  ntrval2  22555  ordtuni  22694  cnclima  22772  cmpsub  22904  ptbasfi  23085  txbasval  23110  pt1hmeo  23310  alexsubALTlem1  23551  trust  23734  ussid  23765  ressuss  23767  ressprdsds  23877  imasdsf1olem  23879  setsms  23988  tmsxms  23995  tmsxpsmopn  24046  subgnm  24142  tngnm  24168  tngngp2  24169  xrsxmet  24325  xrge0gsumle  24349  metdstri  24367  xrhmeo  24462  lebnumlem3  24479  pcorevlem  24542  pi1xfrcnvlem  24572  clmabs  24599  cvsmuleqdivd  24650  rrxip  24907  rrxds  24910  rrxdsfi  24928  minveclem4a  24947  pjthlem1  24954  divcncf  24964  ovolunlem1a  25013  mbfres2  25162  i1faddlem  25210  ibladdlem  25337  iblabs  25346  ditgsplit  25378  dvmptresicc  25433  dvnres  25448  dvmptdiv  25491  dveflem  25496  dveq0  25517  dvfsumabs  25540  itgsubstlem  25565  ply1divex  25654  dgrco  25789  plycjlem  25790  taylthlem1  25885  pserdv2  25942  abelthlem6  25948  abelthlem7  25950  tangtx  26015  abssinper  26030  sineq0  26033  explog  26102  reexplog  26103  eflogeq  26110  abslogle  26126  tanarg  26127  logtayl  26168  logtayl2  26170  relogbdiv  26284  ang180lem3  26316  affineequiv  26328  affineequiv2  26329  chordthmlem4  26340  chordthmlem5  26341  heron  26343  dcubic1lem  26348  dcubic2  26349  dcubic  26351  mcubic  26352  cubic2  26353  dquartlem1  26356  dquart  26358  quart1lem  26360  quartlem1  26362  quart  26366  acoscos  26398  atanlogaddlem  26418  atantayl2  26443  atantayl3  26444  birthdaylem2  26457  efrlim  26474  amgmlem  26494  logdifbnd  26498  emcllem3  26502  emcllem6  26505  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  gamigam  26557  lgamcvg2  26559  gamfac  26571  basellem3  26587  basellem8  26592  basellem9  26593  chtprm  26657  logfaclbnd  26725  perfect1  26731  bcp1ctr  26782  bclbnd  26783  bposlem1  26787  lgsdilem  26827  lgsdirnn0  26847  lgsdinn0  26848  gausslemma2dlem1a  26868  gausslemma2dlem4  26872  gausslemma2dlem5a  26873  lgseisenlem2  26879  lgsquadlem1  26883  2sqlem2  26921  mul2sq  26922  2sqmod  26939  2sqnn0  26941  vmadivsum  26985  rpvmasumlem  26990  dchrisumlem1  26992  dchrisumlem2  26993  dchrmusum2  26997  dchrvmasum2if  27000  dchrisum0lem2  27021  logsqvma2  27046  selberg3  27062  selberg4lem1  27063  pntrsumo1  27068  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem5  27084  pntibndlem2  27094  pntlemk  27109  pntlemo  27110  ostth2lem4  27139  ostth3  27141  tgbtwndiff  27757  tgifscgr  27759  trgcgrg  27766  motcgr3  27796  tgbtwnconn1lem1  27823  tgbtwnconn1lem2  27824  ismir  27910  miriso  27921  midexlem  27943  ragmir  27951  footexALT  27969  footexlem1  27970  footexlem2  27971  colperpexlem3  27983  mideulem2  27985  midex  27988  opphllem3  28000  midcgr  28031  lmiisolem  28047  brbtwn2  28163  colinearalglem4  28167  axsegconlem1  28175  axpaschlem  28198  axcontlem4  28225  axcontlem7  28228  axcontlem8  28229  ushgredgedgloop  28488  crctcshwlkn0lem6  29069  wwlknlsw  29101  wwlksnextwrd  29151  clwlkclwwlklem2a3  29247  clwlkclwwlk2  29256  clwwlkel  29299  clwwlkfo  29303  clwwlkext2edg  29309  eupth2eucrct  29470  numclwwlk2lem1lem  29595  numclwwlk1lem2fo  29611  numclwlk2lem2f  29630  grpoidinvlem2  29758  nvmtri  29924  cnnvm  29935  nvnd  29941  ipidsq  29963  ipnm  29964  ipipcj  29968  blocnilem  30057  ipasslem2  30085  dipsubdir  30101  hvaddsubval  30286  pjhthlem1  30644  pjspansn  30830  pjo  30924  unoplin  31173  adjadj  31189  hmoplin  31195  eigvec1  31215  lnopeqi  31261  nmcexi  31279  lnfnsubi  31299  riesz3i  31315  kbass6  31374  leoprf2  31380  leoprf  31381  pjnmopi  31401  mdslmd1lem1  31578  mdslmd1lem2  31579  superpos  31607  ifeq3da  31778  fgreu  31897  resf1o  31955  fprodex01  32031  wrdt2ind  32117  gsummpt2d  32201  xrge0tsmseq  32211  symgfcoeu  32243  psgnfzto1stlem  32259  psgnfzto1st  32264  cycpm2tr  32278  cycpmco2lem6  32290  cycpmco2lem7  32291  subrgchr  32386  rhmdvd  32436  qusrn  32520  nsgqusf1olem3  32526  rhmquskerlem  32543  elrspunsn  32547  mxidlirredi  32587  qsdrngi  32609  evls1addd  32648  evls1muld  32649  evls1vsca  32650  ply1chr  32661  dimval  32686  dimvalfi  32687  lindsunlem  32709  dimkerim  32712  qusdimsum  32713  fedgmullem1  32714  extdg1id  32742  evls1maprhm  32759  evls1maplmhm  32760  evls1maprnss  32761  ply1annidllem  32762  algextdeglem1  32772  madjusmdetlem2  32808  qtophaus  32816  zarclssn  32853  zarcmplem  32861  pstmval  32875  mndpluscn  32906  qqhucn  32972  esumval  33044  gsumesum  33057  esumcst  33061  esumpcvgval  33076  oddpwdc  33353  eulerpartlemgvv  33375  probdif  33419  sgnmul  33541  signsvtn  33595  actfunsnf1o  33616  reprpmtf1o  33638  hgt750lemd  33660  logdivsqrle  33662  hgt750lemg  33666  hgt750lemb  33668  bnj1415  34049  swrdrevpfx  34107  pfxwlk  34114  derangen2  34165  subfaclefac  34167  subfaclim  34179  satom  34347  fmla  34372  mrsubrn  34504  sinccvglem  34657  bcprod  34708  filnetlem4  35266  curunc  36470  ltflcei  36476  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem24  36512  mblfinlem4  36528  ibladdnclem  36544  iblabsnc  36552  iblmulc2nc  36553  ftc1anclem6  36566  ftc1anclem8  36568  sdclem2  36610  ismtycnv  36670  heiborlem10  36688  lflvsass  37951  lkrscss  37968  eqlkr  37969  eqlkr3  37971  ldualvsdi2  38014  omllaw3  38115  cmtcomlemN  38118  cmtbr3N  38124  omlfh3N  38129  llnexchb2lem  38739  dalawlem7  38748  dalawlem11  38752  dalawlem12  38753  pol1N  38781  paddatclN  38820  4atexlemcnd  38943  ltrncoidN  38999  cdleme3b  39100  cdleme11  39141  cdleme15a  39145  cdleme22e  39215  cdleme22g  39219  cdlemg18b  39550  trlcoat  39594  cdlemk2  39703  cdlemk4  39705  cdlemki  39712  cdlemksv2  39718  cdlemk15  39726  cdlemk55a  39830  diainN  39928  dia2dimlem3  39937  dia2dimlem5  39939  dvhlveclem  39979  diaocN  39996  cdlemn4  40069  cdlemn8  40075  dihopelvalcpre  40119  dihmeetlem9N  40186  dih1dimatlem  40200  dihpN  40207  dochvalr3  40234  dochsat  40254  djhjlj  40274  dochdmm1  40281  dihjatcclem4  40292  dihjat1  40300  dihjat4  40304  dochsnkr2cl  40345  dochfl1  40347  lclkrlem2j  40387  mapdordlem2  40508  mapdrvallem2  40516  hdmap10  40711  lcmineqlem12  40905  3lexlogpow5ineq5  40925  aks4d1p1  40941  frlmvscadiccat  41080  grpcominv1  41082  riccrng1  41096  ricdrng1  41102  frlmsnic  41110  evlselv  41159  fsuppind  41162  nicomachus  41210  sumcubes  41211  cnreeu  41341  flt4lem7  41401  negexpidd  41420  3cubeslem2  41423  3cubeslem3r  41425  mzpsubmpt  41481  irrapxlem3  41562  pellexlem6  41572  pell1234qrne0  41591  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell14qrdich  41607  pell1qrgaplem  41611  rmxluc  41675  rmyluc  41676  jm2.24nn  41698  jm2.18  41727  jm2.19lem2  41729  jm2.19lem3  41730  jm2.22  41734  jm2.23  41735  jm2.16nn0  41743  jm2.27c  41746  fnwe2lem2  41793  lmhmfgsplit  41828  hbtlem2  41866  onsucf1lem  42019  ofoafo  42106  naddcnffo  42114  naddwordnexlem4  42152  reabssgn  42387  relexpmulnn  42460  relexpmulg  42461  ntrclsneine0lem  42815  int-addassocd  42926  dvconstbi  43093  bccm1k  43101  binomcxplemnotnn0  43115  fmptsnxp  43865  wessf1ornlem  43882  projf1o  43896  infnsuprnmpt  43954  lefldiveq  44002  lt4addmuld  44016  fzdifsuc2  44020  suplesup  44049  infrpge  44061  xrlexaddrp  44062  xralrple2  44064  infleinflem1  44080  supminfrnmpt  44155  supminfxr2  44179  fsumnncl  44288  limcperiod  44344  sumnnodd  44346  limcresiooub  44358  limcresioolb  44359  0ellimcdiv  44365  reclimc  44369  limsupval3  44408  limsupequzmpt2  44434  liminfval5  44481  limsupresxr  44482  liminfresxr  44483  liminfvalxr  44499  liminfequzmpt2  44507  climliminflimsupd  44517  liminfltlem  44520  liminflbuz2  44531  sinmulcos  44581  coskpi2  44582  cncfdmsn  44606  cncfiooicclem1  44609  fprodsubrecnncnvlem  44623  fprodaddrecnncnvlem  44625  fperdvper  44635  dvnmptdivc  44654  dvnxpaek  44658  dvnmul  44659  dvnprodlem1  44662  dvnprodlem3  44664  itgcoscmulx  44685  itgsincmulx  44690  itgspltprt  44695  itgiccshift  44696  itgperiod  44697  sublevolico  44700  volioof  44703  ovolsplit  44704  fvvolioof  44705  fvvolicof  44707  stoweidlem22  44738  stoweidlem32  44748  wallispilem5  44785  stirlinglem5  44794  dirkertrigeqlem2  44815  dirkertrigeq  44817  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem13  44836  fourierdlem16  44839  fourierdlem19  44842  fourierdlem21  44844  fourierdlem22  44845  fourierdlem28  44851  fourierdlem32  44855  fourierdlem33  44856  fourierdlem42  44865  fourierdlem47  44869  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem56  44878  fourierdlem60  44882  fourierdlem61  44883  fourierdlem64  44886  fourierdlem66  44888  fourierdlem71  44893  fourierdlem73  44895  fourierdlem74  44896  fourierdlem76  44898  fourierdlem78  44900  fourierdlem79  44901  fourierdlem80  44902  fourierdlem81  44903  fourierdlem83  44905  fourierdlem88  44910  fourierdlem92  44914  fourierdlem93  44915  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem109  44931  fourierdlem111  44933  fouriersw  44947  elaa2lem  44949  etransclem24  44974  etransclem25  44975  etransclem35  44985  etransclem46  44996  rrndistlt  45006  rrxunitopnfi  45008  qndenserrnbl  45011  qndenserrnopnlem  45013  saldifcl2  45044  intsal  45046  sge0sn  45095  sge0ltfirp  45116  sge0iunmptlemre  45131  sge0fodjrnlem  45132  sge0isum  45143  sge0xaddlem1  45149  nnfoctbdjlem  45171  meassle  45179  ismeannd  45183  meadif  45195  meaiuninclem  45196  meaiininclem  45202  omeunile  45221  caragendifcl  45230  caratheodory  45244  isomenndlem  45246  ovnsubaddlem1  45286  hoidmv1lelem2  45308  hoidmv1le  45310  hoidmvlelem2  45312  hoidmvle  45316  hoi2toco  45323  rrnmbl  45330  hoidifhspdmvle  45336  voncmpl  45337  hoiqssbl  45341  hspmbllem1  45342  hspmbllem2  45343  ovolval2lem  45359  ovolval5lem2  45369  ovnovollem1  45372  ovnovollem2  45373  hoimbl2  45381  vonhoire  45388  salpreimagelt  45423  salpreimalegt  45425  preimaioomnf  45435  smfres  45506  smfmullem1  45507  smflimmpt  45526  smfsupmpt  45531  smfinfmpt  45535  smflimsupmpt  45545  smfliminflem  45546  smfliminfmpt  45548  sigarcol  45580  f1oresf1o  45998  elsprel  46143  prproropf1o  46175  paireqne  46179  sfprmdvdsmersenne  46271  lighneallem3  46275  lighneallem4  46278  nn0onn0exALTV  46367  nnsum3primesprm  46458  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  c0snmgmhm  46713  rngqiprnglin  46787  rngcifuestrc  46895  funcrngcsetc  46896  funcrngcsetcALT  46897  funcringcsetc  46933  funcringcsetcALTV2lem7  46940  funcringcsetclem7ALTV  46963  lincext3  47137  lincresunit3  47162  nn0onn0ex  47209  nnpw2pmod  47269  blennn0em1  47277  digexp  47293  dignn0ehalf  47303  nn0mulfsum  47310  itcovalpclem1  47356  eenglngeehlnmlem2  47424  rrx2vlinest  47427  line2  47438  itschlc0xyqsol  47453  itsclinecirc0b  47460  toplatjoin  47627  toplatmeet  47628  recsec  47801  reccsc  47802  aacllem  47848  amgmlemALT  47850