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  sltonold  27690  tgbtwndiff  27788  tgifscgr  27790  trgcgrg  27797  motcgr3  27827  tgbtwnconn1lem1  27854  tgbtwnconn1lem2  27855  ismir  27941  miriso  27952  midexlem  27974  ragmir  27982  footexALT  28000  footexlem1  28001  footexlem2  28002  colperpexlem3  28014  mideulem2  28016  midex  28019  opphllem3  28031  midcgr  28062  lmiisolem  28078  brbtwn2  28194  colinearalglem4  28198  axsegconlem1  28206  axpaschlem  28229  axcontlem4  28256  axcontlem7  28259  axcontlem8  28260  ushgredgedgloop  28519  crctcshwlkn0lem6  29100  wwlknlsw  29132  wwlksnextwrd  29182  clwlkclwwlklem2a3  29278  clwlkclwwlk2  29287  clwwlkel  29330  clwwlkfo  29334  clwwlkext2edg  29340  eupth2eucrct  29501  numclwwlk2lem1lem  29626  numclwwlk1lem2fo  29642  numclwlk2lem2f  29661  grpoidinvlem2  29789  nvmtri  29955  cnnvm  29966  nvnd  29972  ipidsq  29994  ipnm  29995  ipipcj  29999  blocnilem  30088  ipasslem2  30116  dipsubdir  30132  hvaddsubval  30317  pjhthlem1  30675  pjspansn  30861  pjo  30955  unoplin  31204  adjadj  31220  hmoplin  31226  eigvec1  31246  lnopeqi  31292  nmcexi  31310  lnfnsubi  31330  riesz3i  31346  kbass6  31405  leoprf2  31411  leoprf  31412  pjnmopi  31432  mdslmd1lem1  31609  mdslmd1lem2  31610  superpos  31638  ifeq3da  31809  fgreu  31928  resf1o  31986  fprodex01  32062  wrdt2ind  32148  gsummpt2d  32232  xrge0tsmseq  32242  symgfcoeu  32274  psgnfzto1stlem  32290  psgnfzto1st  32295  cycpm2tr  32309  cycpmco2lem6  32321  cycpmco2lem7  32322  subrgchr  32417  rhmdvd  32467  qusrn  32551  nsgqusf1olem3  32557  rhmquskerlem  32574  elrspunsn  32578  mxidlirredi  32618  qsdrngi  32640  evls1addd  32679  evls1muld  32680  evls1vsca  32681  ply1chr  32692  dimval  32717  dimvalfi  32718  lindsunlem  32740  dimkerim  32743  qusdimsum  32744  fedgmullem1  32745  extdg1id  32773  evls1maprhm  32790  evls1maplmhm  32791  evls1maprnss  32792  ply1annidllem  32793  algextdeglem1  32803  madjusmdetlem2  32839  qtophaus  32847  zarclssn  32884  zarcmplem  32892  pstmval  32906  mndpluscn  32937  qqhucn  33003  esumval  33075  gsumesum  33088  esumcst  33092  esumpcvgval  33107  oddpwdc  33384  eulerpartlemgvv  33406  probdif  33450  sgnmul  33572  signsvtn  33626  actfunsnf1o  33647  reprpmtf1o  33669  hgt750lemd  33691  logdivsqrle  33693  hgt750lemg  33697  hgt750lemb  33699  bnj1415  34080  swrdrevpfx  34138  pfxwlk  34145  derangen2  34196  subfaclefac  34198  subfaclim  34210  satom  34378  fmla  34403  mrsubrn  34535  sinccvglem  34688  bcprod  34739  filnetlem4  35314  curunc  36518  ltflcei  36524  matunitlindflem1  36532  matunitlindflem2  36533  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem24  36560  mblfinlem4  36576  ibladdnclem  36592  iblabsnc  36600  iblmulc2nc  36601  ftc1anclem6  36614  ftc1anclem8  36616  sdclem2  36658  ismtycnv  36718  heiborlem10  36736  lflvsass  37999  lkrscss  38016  eqlkr  38017  eqlkr3  38019  ldualvsdi2  38062  omllaw3  38163  cmtcomlemN  38166  cmtbr3N  38172  omlfh3N  38177  llnexchb2lem  38787  dalawlem7  38796  dalawlem11  38800  dalawlem12  38801  pol1N  38829  paddatclN  38868  4atexlemcnd  38991  ltrncoidN  39047  cdleme3b  39148  cdleme11  39189  cdleme15a  39193  cdleme22e  39263  cdleme22g  39267  cdlemg18b  39598  trlcoat  39642  cdlemk2  39751  cdlemk4  39753  cdlemki  39760  cdlemksv2  39766  cdlemk15  39774  cdlemk55a  39878  diainN  39976  dia2dimlem3  39985  dia2dimlem5  39987  dvhlveclem  40027  diaocN  40044  cdlemn4  40117  cdlemn8  40123  dihopelvalcpre  40167  dihmeetlem9N  40234  dih1dimatlem  40248  dihpN  40255  dochvalr3  40282  dochsat  40302  djhjlj  40322  dochdmm1  40329  dihjatcclem4  40340  dihjat1  40348  dihjat4  40352  dochsnkr2cl  40393  dochfl1  40395  lclkrlem2j  40435  mapdordlem2  40556  mapdrvallem2  40564  hdmap10  40759  lcmineqlem12  40953  3lexlogpow5ineq5  40973  aks4d1p1  40989  frlmvscadiccat  41128  grpcominv1  41130  riccrng1  41144  ricdrng1  41150  frlmsnic  41158  evlselv  41207  fsuppind  41210  nicomachus  41258  sumcubes  41259  cnreeu  41389  flt4lem7  41449  negexpidd  41468  3cubeslem2  41471  3cubeslem3r  41473  mzpsubmpt  41529  irrapxlem3  41610  pellexlem6  41620  pell1234qrne0  41639  pell1234qrreccl  41640  pell1234qrmulcl  41641  pell14qrdich  41655  pell1qrgaplem  41659  rmxluc  41723  rmyluc  41724  jm2.24nn  41746  jm2.18  41775  jm2.19lem2  41777  jm2.19lem3  41778  jm2.22  41782  jm2.23  41783  jm2.16nn0  41791  jm2.27c  41794  fnwe2lem2  41841  lmhmfgsplit  41876  hbtlem2  41914  onsucf1lem  42067  ofoafo  42154  naddcnffo  42162  naddwordnexlem4  42200  reabssgn  42435  relexpmulnn  42508  relexpmulg  42509  ntrclsneine0lem  42863  int-addassocd  42974  dvconstbi  43141  bccm1k  43149  binomcxplemnotnn0  43163  fmptsnxp  43913  wessf1ornlem  43930  projf1o  43944  infnsuprnmpt  44002  lefldiveq  44050  lt4addmuld  44064  fzdifsuc2  44068  suplesup  44097  infrpge  44109  xrlexaddrp  44110  xralrple2  44112  infleinflem1  44128  supminfrnmpt  44203  supminfxr2  44227  fsumnncl  44336  limcperiod  44392  sumnnodd  44394  limcresiooub  44406  limcresioolb  44407  0ellimcdiv  44413  reclimc  44417  limsupval3  44456  limsupequzmpt2  44482  liminfval5  44529  limsupresxr  44530  liminfresxr  44531  liminfvalxr  44547  liminfequzmpt2  44555  climliminflimsupd  44565  liminfltlem  44568  liminflbuz2  44579  sinmulcos  44629  coskpi2  44630  cncfdmsn  44654  cncfiooicclem1  44657  fprodsubrecnncnvlem  44671  fprodaddrecnncnvlem  44673  fperdvper  44683  dvnmptdivc  44702  dvnxpaek  44706  dvnmul  44707  dvnprodlem1  44710  dvnprodlem3  44712  itgcoscmulx  44733  itgsincmulx  44738  itgspltprt  44743  itgiccshift  44744  itgperiod  44745  sublevolico  44748  volioof  44751  ovolsplit  44752  fvvolioof  44753  fvvolicof  44755  stoweidlem22  44786  stoweidlem32  44796  wallispilem5  44833  stirlinglem5  44842  dirkertrigeqlem2  44863  dirkertrigeq  44865  dirkercncflem1  44867  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem13  44884  fourierdlem16  44887  fourierdlem19  44890  fourierdlem21  44892  fourierdlem22  44893  fourierdlem28  44899  fourierdlem32  44903  fourierdlem33  44904  fourierdlem42  44913  fourierdlem47  44917  fourierdlem48  44918  fourierdlem49  44919  fourierdlem50  44920  fourierdlem56  44926  fourierdlem60  44930  fourierdlem61  44931  fourierdlem64  44934  fourierdlem66  44936  fourierdlem71  44941  fourierdlem73  44943  fourierdlem74  44944  fourierdlem76  44946  fourierdlem78  44948  fourierdlem79  44949  fourierdlem80  44950  fourierdlem81  44951  fourierdlem83  44953  fourierdlem88  44958  fourierdlem92  44962  fourierdlem93  44963  fourierdlem97  44967  fourierdlem101  44971  fourierdlem103  44973  fourierdlem104  44974  fourierdlem109  44979  fourierdlem111  44981  fouriersw  44995  elaa2lem  44997  etransclem24  45022  etransclem25  45023  etransclem35  45033  etransclem46  45044  rrndistlt  45054  rrxunitopnfi  45056  qndenserrnbl  45059  qndenserrnopnlem  45061  saldifcl2  45092  intsal  45094  sge0sn  45143  sge0ltfirp  45164  sge0iunmptlemre  45179  sge0fodjrnlem  45180  sge0isum  45191  sge0xaddlem1  45197  nnfoctbdjlem  45219  meassle  45227  ismeannd  45231  meadif  45243  meaiuninclem  45244  meaiininclem  45250  omeunile  45269  caragendifcl  45278  caratheodory  45292  isomenndlem  45294  ovnsubaddlem1  45334  hoidmv1lelem2  45356  hoidmv1le  45358  hoidmvlelem2  45360  hoidmvle  45364  hoi2toco  45371  rrnmbl  45378  hoidifhspdmvle  45384  voncmpl  45385  hoiqssbl  45389  hspmbllem1  45390  hspmbllem2  45391  ovolval2lem  45407  ovolval5lem2  45417  ovnovollem1  45420  ovnovollem2  45421  hoimbl2  45429  vonhoire  45436  salpreimagelt  45471  salpreimalegt  45473  preimaioomnf  45483  smfres  45554  smfmullem1  45555  smflimmpt  45574  smfsupmpt  45579  smfinfmpt  45583  smflimsupmpt  45593  smfliminflem  45594  smfliminfmpt  45596  sigarcol  45628  f1oresf1o  46046  elsprel  46191  prproropf1o  46223  paireqne  46227  sfprmdvdsmersenne  46319  lighneallem3  46323  lighneallem4  46326  nn0onn0exALTV  46415  nnsum3primesprm  46506  nnsum4primesodd  46512  nnsum4primesoddALTV  46513  c0snmgmhm  46761  rngqiprnglin  46835  rngcifuestrc  46943  funcrngcsetc  46944  funcrngcsetcALT  46945  funcringcsetc  46981  funcringcsetcALTV2lem7  46988  funcringcsetclem7ALTV  47011  lincext3  47185  lincresunit3  47210  nn0onn0ex  47257  nnpw2pmod  47317  blennn0em1  47325  digexp  47341  dignn0ehalf  47351  nn0mulfsum  47358  itcovalpclem1  47404  eenglngeehlnmlem2  47472  rrx2vlinest  47475  line2  47486  itschlc0xyqsol  47501  itsclinecirc0b  47508  toplatjoin  47675  toplatmeet  47676  recsec  47849  reccsc  47850  aacllem  47896  amgmlemALT  47898