Theorem eqtr2d 2766

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  3eqtrrd  2770  3eqtr2rd  2772  ifan  4545  ifor  4546  dfopif  4837  fnco  6639  fnsnfv  6943  nvocnv  7259  elovmpt3rab1  7652  onsucmin  7799  csbopeq1a  8032  oaabs2  8616  ecinxp  8768  resixpfo  8912  sbthlem3  9059  rankxpsuc  9842  fseqenlem2  9985  dfac2b  10091  isf32lem9  10321  compsscnvlem  10330  ttukeylem7  10475  fpwwe2lem10  10600  00id  11356  submul2  11625  mulsubfacd  11646  divadddiv  11904  infrenegsup  12173  xadd4d  13270  fzdifsuc  13552  fzval3  13702  fzoshftral  13752  ceim1l  13816  fldiv  13829  flmod  13854  intfrac  13855  modcyc2  13876  modaddb  13878  moddi  13911  uzrdgfni  13930  axdc4uzlem  13955  seqf1olem1  14013  seqf1olem2  14014  seqid2  14020  expnegz  14068  binom2sub  14192  binom3  14196  hashreshashfun  14411  ccatw2s1p2  14609  ccats1pfxeq  14686  pfxccatin12lem2  14703  pfxccatin12  14705  swrdccat3b  14712  cshweqrep  14793  2cshwcshw  14798  ccatco  14808  swrds2  14913  relexpsucnnr  14998  relexpaddnn  15024  reim  15082  mulre  15094  addcj  15121  absimle  15282  clim2ser  15628  isercoll2  15642  serf0  15654  iseralt  15658  summolem3  15687  isumclim3  15732  mptfzshft  15751  fsumrev  15752  fsum2mul  15762  incexc  15810  isumsplit  15813  mertenslem1  15857  fprodrev  15950  iprodclim3  15973  binomfallfaclem2  16013  ef4p  16088  tanval3  16109  efival  16127  sinmul  16147  bitsinvp1  16426  sadaddlem  16443  bitsshft  16452  smu01lem  16462  dfgcd2  16523  lcmgcdlem  16583  lcm1  16587  lcmfass  16623  eulerthlem2  16759  hashgcdeq  16767  powm2modprm  16781  pythagtriplem16  16808  pczpre  16825  pcqdiv  16835  pcadd  16867  pcfac  16877  prmreclem5  16898  4sqlem10  16925  4sqlem19  16941  vdwapun  16952  vdwlem1  16959  ramcl  17007  setsstruct  17153  strfvd  17177  strfv2d  17178  xpsff1o  17537  xpsrnbas  17541  2oppccomf  17693  oppcepi  17708  sscfn1  17786  sscfn2  17787  invfuc  17946  funcestrcsetclem7  18114  funcsetcestrclem7  18129  gsumsplit1r  18621  grpinvssd  18956  grpinvval2  18962  cycsubggend  19144  pmtrdifwrdellem2  19419  psgnunilem1  19430  psgnuni  19436  pgp0  19533  sylow1lem1  19535  sylow3lem2  19565  efgredleme  19680  efgcpbllemb  19692  frgpuptinv  19708  frgpup3lem  19714  gexexlem  19789  cyggenod  19821  gsumval3eu  19841  gsumval3  19844  gsumzaddlem  19858  dprd2db  19982  ablsimpgfindlem1  20046  ringinvdv  20330  c0snmgmhm  20378  rngcifuestrc  20555  funcrngcsetc  20556  funcrngcsetcALT  20557  funcringcsetc  20590  lss1d  20876  pwssplit1  20973  rhmqusnsg  21202  rngqiprnglin  21219  znzrh2  21462  regsumsupp  21538  ipassr2  21563  dsmmfi  21654  frlmlss  21667  frlmip  21694  frlmlbs  21713  frlmup3  21716  islindf4  21754  mplcoe3  21952  subrgascl  21980  evlseu  21997  psdadd  22057  ply1sclid  22181  ply1chr  22200  evls1addd  22265  evls1muld  22266  evls1vsca  22267  evls1maprhm  22270  evls1maplmhm  22271  evls1maprnss  22272  evl1maprhm  22273  1marepvmarrepid  22469  madurid  22538  smadiadetlem3  22562  mat2pmatghm  22624  pmatcollpwscmatlem1  22683  pm2mpmhmlem2  22713  cpmadurid  22761  cpmidgsumm2pm  22763  cpmadugsumlemB  22768  cayhamlem2  22778  ntrval2  22945  ordtuni  23084  cnclima  23162  cmpsub  23294  ptbasfi  23475  txbasval  23500  pt1hmeo  23700  alexsubALTlem1  23941  trust  24124  ussid  24155  ressuss  24157  ressprdsds  24266  imasdsf1olem  24268  setsms  24375  tmsxms  24381  tmsxpsmopn  24432  subgnm  24528  tngnm  24546  tngngp2  24547  xrsxmet  24705  xrge0gsumle  24729  metdstri  24747  xrhmeo  24851  lebnumlem3  24869  pcorevlem  24933  pi1xfrcnvlem  24963  clmabs  24990  cvsmuleqdivd  25041  rrxip  25297  rrxds  25300  rrxdsfi  25318  minveclem4a  25337  pjthlem1  25344  divcncf  25355  ovolunlem1a  25404  mbfres2  25553  i1faddlem  25601  ibladdlem  25728  iblabs  25737  ditgsplit  25769  dvmptresicc  25824  dvnres  25840  dvmptdiv  25885  dveflem  25890  dveq0  25912  dvfsumabs  25936  itgsubstlem  25962  ply1divex  26049  r1pid2  26074  dgrco  26188  plycjlem  26189  taylthlem1  26288  pserdv2  26347  abelthlem6  26353  abelthlem7  26355  tangtx  26421  abssinper  26437  sineq0  26440  explog  26510  reexplog  26511  eflogeq  26518  abslogle  26534  tanarg  26535  logtayl  26576  logtayl2  26578  relogbdiv  26696  ang180lem3  26728  affineequiv  26740  affineequiv2  26741  chordthmlem4  26752  chordthmlem5  26753  heron  26755  dcubic1lem  26760  dcubic2  26761  dcubic  26763  mcubic  26764  cubic2  26765  dquartlem1  26768  dquart  26770  quart1lem  26772  quartlem1  26774  quart  26778  acoscos  26810  atanlogaddlem  26830  atantayl2  26855  atantayl3  26856  birthdaylem2  26869  efrlim  26886  efrlimOLD  26887  amgmlem  26907  logdifbnd  26911  emcllem3  26915  emcllem6  26918  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  gamigam  26970  lgamcvg2  26972  gamfac  26984  basellem3  27000  basellem8  27005  basellem9  27006  chtprm  27070  logfaclbnd  27140  perfect1  27146  bcp1ctr  27197  bclbnd  27198  bposlem1  27202  lgsdilem  27242  lgsdirnn0  27262  lgsdinn0  27263  gausslemma2dlem1a  27283  gausslemma2dlem4  27287  gausslemma2dlem5a  27288  lgseisenlem2  27294  lgsquadlem1  27298  2sqlem2  27336  mul2sq  27337  2sqmod  27354  2sqnn0  27356  vmadivsum  27400  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrmusum2  27412  dchrvmasum2if  27415  dchrisum0lem2  27436  logsqvma2  27461  selberg3  27477  selberg4lem1  27478  pntrsumo1  27483  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntibndlem2  27509  pntlemk  27524  pntlemo  27525  ostth2lem4  27554  ostth3  27556  subsfo  27976  negsval2  27977  sltonold  28169  noseqrdgfn  28207  n0sfincut  28253  addhalfcut  28341  tgbtwndiff  28440  tgifscgr  28442  trgcgrg  28449  motcgr3  28479  tgbtwnconn1lem1  28506  tgbtwnconn1lem2  28507  ismir  28593  miriso  28604  midexlem  28626  ragmir  28634  footexALT  28652  footexlem1  28653  footexlem2  28654  colperpexlem3  28666  mideulem2  28668  midex  28671  opphllem3  28683  midcgr  28714  lmiisolem  28730  brbtwn2  28839  colinearalglem4  28843  axsegconlem1  28851  axpaschlem  28874  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  ushgredgedgloop  29165  crctcshwlkn0lem6  29752  wwlknlsw  29784  wwlksnextwrd  29834  clwlkclwwlklem2a3  29930  clwlkclwwlk2  29939  clwwlkel  29982  clwwlkfo  29986  clwwlkext2edg  29992  eupth2eucrct  30153  numclwwlk2lem1lem  30278  numclwwlk1lem2fo  30294  numclwlk2lem2f  30313  grpoidinvlem2  30441  nvmtri  30607  cnnvm  30618  nvnd  30624  ipidsq  30646  ipnm  30647  ipipcj  30651  blocnilem  30740  ipasslem2  30768  dipsubdir  30784  hvaddsubval  30969  pjhthlem1  31327  pjspansn  31513  pjo  31607  unoplin  31856  adjadj  31872  hmoplin  31878  eigvec1  31898  lnopeqi  31944  nmcexi  31962  lnfnsubi  31982  riesz3i  31998  kbass6  32057  leoprf2  32063  leoprf  32064  pjnmopi  32084  mdslmd1lem1  32261  mdslmd1lem2  32262  superpos  32290  ifeq3da  32482  fgreu  32603  resf1o  32660  quad3d  32680  fprodex01  32757  sgnmul  32767  ccatws1f1o  32880  wrdt2ind  32882  mndlactfo  32975  mndractfo  32977  gsummpt2d  32996  xrge0tsmseq  33011  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  symgfcoeu  33046  wrdpmtrlast  33057  psgnfzto1stlem  33064  psgnfzto1st  33069  cycpm2tr  33083  cycpmco2lem6  33095  cycpmco2lem7  33096  subrgchr  33195  elrgspnlem1  33200  elrgspnlem3  33202  elrgspnsubrunlem1  33205  rloccring  33228  rhmdvd  33303  qusrn  33387  nsgqusf1olem3  33393  rhmquskerlem  33403  elrspunsn  33407  mxidlirredi  33449  qsdrngi  33473  1arithidomlem1  33513  1arithidomlem2  33514  evls1subd  33548  r1pid2OLD  33581  resssra  33590  dimval  33603  dimvalfi  33604  lindsunlem  33627  dimkerim  33630  qusdimsum  33631  fedgmullem1  33632  extdg1id  33668  fldextrspunlsplem  33675  fldextrspunlsp  33676  fldextrspunlem1  33677  fldextrspundgdvds  33683  ply1annidllem  33698  algextdeglem4  33717  constrrtcc  33732  constrsslem  33738  constrresqrtcl  33774  cos9thpiminplylem2  33780  cos9thpiminply  33785  madjusmdetlem2  33825  qtophaus  33833  zarclssn  33870  zarcmplem  33878  pstmval  33892  mndpluscn  33923  qqhucn  33989  esumval  34043  gsumesum  34056  esumcst  34060  esumpcvgval  34075  oddpwdc  34352  eulerpartlemgvv  34374  probdif  34418  signsvtn  34582  actfunsnf1o  34602  reprpmtf1o  34624  hgt750lemd  34646  logdivsqrle  34648  hgt750lemg  34652  hgt750lemb  34654  bnj1415  35035  swrdrevpfx  35111  pfxwlk  35118  derangen2  35168  subfaclefac  35170  subfaclim  35182  satom  35350  fmla  35375  mrsubrn  35507  sinccvglem  35666  bcprod  35732  filnetlem4  36376  curunc  37603  ltflcei  37609  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem24  37645  mblfinlem4  37661  ibladdnclem  37677  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem6  37699  ftc1anclem8  37701  sdclem2  37743  ismtycnv  37803  heiborlem10  37821  lflvsass  39081  lkrscss  39098  eqlkr  39099  eqlkr3  39101  ldualvsdi2  39144  omllaw3  39245  cmtcomlemN  39248  cmtbr3N  39254  omlfh3N  39259  llnexchb2lem  39869  dalawlem7  39878  dalawlem11  39882  dalawlem12  39883  pol1N  39911  paddatclN  39950  4atexlemcnd  40073  ltrncoidN  40129  cdleme3b  40230  cdleme11  40271  cdleme15a  40275  cdleme22e  40345  cdleme22g  40349  cdlemg18b  40680  trlcoat  40724  cdlemk2  40833  cdlemk4  40835  cdlemki  40842  cdlemksv2  40848  cdlemk15  40856  cdlemk55a  40960  diainN  41058  dia2dimlem3  41067  dia2dimlem5  41069  dvhlveclem  41109  diaocN  41126  cdlemn4  41199  cdlemn8  41205  dihopelvalcpre  41249  dihmeetlem9N  41316  dih1dimatlem  41330  dihpN  41337  dochvalr3  41364  dochsat  41384  djhjlj  41404  dochdmm1  41411  dihjatcclem4  41422  dihjat1  41430  dihjat4  41434  dochsnkr2cl  41475  dochfl1  41477  lclkrlem2j  41517  mapdordlem2  41638  mapdrvallem2  41646  hdmap10  41841  lcmineqlem12  42035  3lexlogpow5ineq5  42055  aks4d1p1  42071  primrootsunit1  42092  primrootscoprmpow  42094  posbezout  42095  aks6d1c1p3  42105  aks6d1c1p4  42106  aks6d1c1p5  42107  aks6d1c1p7  42108  evl1gprodd  42112  hashscontpow1  42116  aks6d1c3  42118  aks6d1c2lem3  42121  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5lem3  42132  aks6d1c6lem1  42165  aks6d1c6isolem3  42171  aks6d1c6lem5  42172  bcle2d  42174  aks6d1c7lem1  42175  aks5lem3a  42184  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem4  42193  unitscyglem5  42194  aks5lem7  42195  nicomachus  42307  sumcubes  42308  cnreeu  42485  frlmvscadiccat  42501  grpcominv1  42503  riccrng1  42516  ricdrng1  42523  frlmsnic  42535  evlselv  42582  fsuppind  42585  flt4lem7  42654  negexpidd  42677  3cubeslem2  42680  3cubeslem3r  42682  mzpsubmpt  42738  irrapxlem3  42819  pellexlem6  42829  pell1234qrne0  42848  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell14qrdich  42864  pell1qrgaplem  42868  rmxluc  42932  rmyluc  42933  jm2.24nn  42955  jm2.18  42984  jm2.19lem2  42986  jm2.19lem3  42987  jm2.22  42991  jm2.23  42992  jm2.16nn0  43000  jm2.27c  43003  fnwe2lem2  43047  lmhmfgsplit  43082  hbtlem2  43120  onsucf1lem  43265  ofoafo  43352  naddcnffo  43360  naddwordnexlem4  43397  reabssgn  43632  relexpmulnn  43705  relexpmulg  43706  ntrclsneine0lem  44060  int-addassocd  44170  dvconstbi  44330  bccm1k  44338  binomcxplemnotnn0  44352  fmptsnxp  45170  wessf1ornlem  45186  projf1o  45198  infnsuprnmpt  45251  lefldiveq  45297  lt4addmuld  45311  fzdifsuc2  45315  suplesup  45342  infrpge  45354  xrlexaddrp  45355  xralrple2  45357  infleinflem1  45373  supminfrnmpt  45448  supminfxr2  45472  fsumnncl  45577  limcperiod  45633  sumnnodd  45635  limcresiooub  45647  limcresioolb  45648  0ellimcdiv  45654  reclimc  45658  limsupval3  45697  limsupequzmpt2  45723  liminfval5  45770  limsupresxr  45771  liminfresxr  45772  liminfvalxr  45788  liminfequzmpt2  45796  climliminflimsupd  45806  liminfltlem  45809  liminflbuz2  45820  sinmulcos  45870  coskpi2  45871  cncfdmsn  45895  cncfiooicclem1  45898  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  fperdvper  45924  dvnmptdivc  45943  dvnxpaek  45947  dvnmul  45948  dvnprodlem1  45951  dvnprodlem3  45953  itgcoscmulx  45974  itgsincmulx  45979  itgspltprt  45984  itgiccshift  45985  itgperiod  45986  sublevolico  45989  volioof  45992  ovolsplit  45993  fvvolioof  45994  fvvolicof  45996  stoweidlem22  46027  stoweidlem32  46037  wallispilem5  46074  stirlinglem5  46083  dirkertrigeqlem2  46104  dirkertrigeq  46106  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem13  46125  fourierdlem16  46128  fourierdlem19  46131  fourierdlem21  46133  fourierdlem22  46134  fourierdlem28  46140  fourierdlem32  46144  fourierdlem33  46145  fourierdlem42  46154  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem56  46167  fourierdlem60  46171  fourierdlem61  46172  fourierdlem64  46175  fourierdlem66  46177  fourierdlem71  46182  fourierdlem73  46184  fourierdlem74  46185  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem80  46191  fourierdlem81  46192  fourierdlem83  46194  fourierdlem88  46199  fourierdlem92  46203  fourierdlem93  46204  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem109  46220  fourierdlem111  46222  fouriersw  46236  elaa2lem  46238  etransclem24  46263  etransclem25  46264  etransclem35  46274  etransclem46  46285  rrndistlt  46295  rrxunitopnfi  46297  qndenserrnbl  46300  qndenserrnopnlem  46302  saldifcl2  46333  intsal  46335  sge0sn  46384  sge0ltfirp  46405  sge0iunmptlemre  46420  sge0fodjrnlem  46421  sge0isum  46432  sge0xaddlem1  46438  nnfoctbdjlem  46460  meassle  46468  ismeannd  46472  meadif  46484  meaiuninclem  46485  meaiininclem  46491  omeunile  46510  caragendifcl  46519  caratheodory  46533  isomenndlem  46535  ovnsubaddlem1  46575  hoidmv1lelem2  46597  hoidmv1le  46599  hoidmvlelem2  46601  hoidmvle  46605  hoi2toco  46612  rrnmbl  46619  hoidifhspdmvle  46625  voncmpl  46626  hoiqssbl  46630  hspmbllem1  46631  hspmbllem2  46632  ovolval2lem  46648  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  hoimbl2  46670  vonhoire  46677  salpreimagelt  46712  salpreimalegt  46714  preimaioomnf  46724  smfres  46795  smfmullem1  46796  smflimmpt  46815  smfsupmpt  46820  smfinfmpt  46824  smflimsupmpt  46834  smfliminflem  46835  smfliminfmpt  46837  sigarcol  46869  f1oresf1o  47295  elsprel  47480  prproropf1o  47512  paireqne  47516  sfprmdvdsmersenne  47608  lighneallem3  47612  lighneallem4  47615  nn0onn0exALTV  47704  nnsum3primesprm  47795  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  isuspgrim0lem  47897  clnbgrgrimlem  47937  uspgrlimlem3  47993  uspgrlimlem4  47994  gpgedgvtx0  48056  gpgedgvtx1  48057  funcringcsetcALTV2lem7  48288  funcringcsetclem7ALTV  48311  lincext3  48449  lincresunit3  48474  nn0onn0ex  48516  nnpw2pmod  48576  blennn0em1  48584  digexp  48600  dignn0ehalf  48610  nn0mulfsum  48617  itcovalpclem1  48663  eenglngeehlnmlem2  48731  rrx2vlinest  48734  line2  48745  itschlc0xyqsol  48760  itsclinecirc0b  48767  toplatjoin  48994  toplatmeet  48995  upeu2lem  49021  oppff1o  49142  imaf1co  49148  upciclem3  49161  natoppfb  49224  oppcthinco  49432  oppcthinendcALT  49434  lmddu  49660  recsec  49749  reccsc  49750  aacllem  49794  amgmlemALT  49796