Theorem eqtr2d 2773

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 2772	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2743	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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtrrd  2777  3eqtr2rd  2779  ifan  4521  ifor  4522  dfopif  4814  fnco  6608  fnsnfv  6911  nvocnv  7227  elovmpt3rab1  7618  onsucmin  7763  csbopeq1a  7994  oaabs2  8576  ecinxp  8730  resixpfo  8875  sbthlem3  9018  rankxpsuc  9795  fseqenlem2  9936  dfac2b  10042  isf32lem9  10272  compsscnvlem  10281  ttukeylem7  10426  fpwwe2lem10  10552  00id  11309  submul2  11578  mulsubfacd  11599  divadddiv  11857  infrenegsup  12126  xadd4d  13219  fzdifsuc  13501  fzval3  13651  fzoshftral  13704  ceim1l  13768  fldiv  13781  flmod  13806  intfrac  13807  modcyc2  13828  modaddb  13830  moddi  13863  uzrdgfni  13882  axdc4uzlem  13907  seqf1olem1  13965  seqf1olem2  13966  seqid2  13972  expnegz  14020  binom2sub  14144  binom3  14148  hashreshashfun  14363  ccatw2s1p2  14562  ccats1pfxeq  14638  pfxccatin12lem2  14655  pfxccatin12  14657  swrdccat3b  14664  cshweqrep  14745  2cshwcshw  14749  ccatco  14759  swrds2  14864  relexpsucnnr  14949  relexpaddnn  14975  reim  15033  mulre  15045  addcj  15072  absimle  15233  clim2ser  15579  isercoll2  15593  serf0  15605  iseralt  15609  summolem3  15638  isumclim3  15683  mptfzshft  15702  fsumrev  15703  fsum2mul  15713  incexc  15761  isumsplit  15764  mertenslem1  15808  fprodrev  15901  iprodclim3  15924  binomfallfaclem2  15964  ef4p  16039  tanval3  16060  efival  16078  sinmul  16098  bitsinvp1  16377  sadaddlem  16394  bitsshft  16403  smu01lem  16413  dfgcd2  16474  lcmgcdlem  16534  lcm1  16538  lcmfass  16574  eulerthlem2  16710  hashgcdeq  16718  powm2modprm  16732  pythagtriplem16  16759  pczpre  16776  pcqdiv  16786  pcadd  16818  pcfac  16828  prmreclem5  16849  4sqlem10  16876  4sqlem19  16892  vdwapun  16903  vdwlem1  16910  ramcl  16958  setsstruct  17104  strfvd  17128  strfv2d  17129  xpsff1o  17489  xpsrnbas  17493  2oppccomf  17649  oppcepi  17664  sscfn1  17742  sscfn2  17743  invfuc  17902  funcestrcsetclem7  18070  funcsetcestrclem7  18085  gsumsplit1r  18613  grpinvssd  18951  grpinvval2  18957  cycsubggend  19138  pmtrdifwrdellem2  19415  psgnunilem1  19426  psgnuni  19432  pgp0  19529  sylow1lem1  19531  sylow3lem2  19561  efgredleme  19676  efgcpbllemb  19688  frgpuptinv  19704  frgpup3lem  19710  gexexlem  19785  cyggenod  19817  gsumval3eu  19837  gsumval3  19840  gsumzaddlem  19854  dprd2db  19978  ablsimpgfindlem1  20042  ringinvdv  20352  c0snmgmhm  20400  rngcifuestrc  20574  funcrngcsetc  20575  funcrngcsetcALT  20576  funcringcsetc  20609  lss1d  20916  pwssplit1  21013  rhmqusnsg  21242  rngqiprnglin  21259  znzrh2  21502  regsumsupp  21579  ipassr2  21604  dsmmfi  21695  frlmlss  21708  frlmip  21735  frlmlbs  21754  frlmup3  21757  islindf4  21795  mplcoe3  21994  subrgascl  22022  evlseu  22039  psdadd  22107  ply1sclid  22231  ply1chr  22249  evls1addd  22314  evls1muld  22315  evls1vsca  22316  evls1maprhm  22319  evls1maplmhm  22320  evls1maprnss  22321  evl1maprhm  22322  1marepvmarrepid  22518  madurid  22587  smadiadetlem3  22611  mat2pmatghm  22673  pmatcollpwscmatlem1  22732  pm2mpmhmlem2  22762  cpmadurid  22810  cpmidgsumm2pm  22812  cpmadugsumlemB  22817  cayhamlem2  22827  ntrval2  22994  ordtuni  23133  cnclima  23211  cmpsub  23343  ptbasfi  23524  txbasval  23549  pt1hmeo  23749  alexsubALTlem1  23990  trust  24172  ussid  24203  ressuss  24205  ressprdsds  24314  imasdsf1olem  24316  setsms  24423  tmsxms  24429  tmsxpsmopn  24480  subgnm  24576  tngnm  24594  tngngp2  24595  xrsxmet  24753  xrge0gsumle  24777  metdstri  24795  xrhmeo  24891  lebnumlem3  24908  pcorevlem  24971  pi1xfrcnvlem  25001  clmabs  25028  cvsmuleqdivd  25079  rrxip  25335  rrxds  25338  rrxdsfi  25356  minveclem4a  25375  pjthlem1  25382  divcncf  25392  ovolunlem1a  25441  mbfres2  25590  i1faddlem  25638  ibladdlem  25765  iblabs  25774  ditgsplit  25806  dvmptresicc  25861  dvnres  25876  dvmptdiv  25919  dveflem  25924  dveq0  25946  dvfsumabs  25970  itgsubstlem  25996  ply1divex  26083  r1pid2  26108  dgrco  26221  plycjlem  26222  taylthlem1  26321  pserdv2  26380  abelthlem6  26386  abelthlem7  26388  tangtx  26454  abssinper  26470  sineq0  26473  explog  26543  reexplog  26544  eflogeq  26551  abslogle  26567  tanarg  26568  logtayl  26609  logtayl2  26611  relogbdiv  26729  ang180lem3  26761  affineequiv  26773  affineequiv2  26774  chordthmlem4  26785  chordthmlem5  26786  heron  26788  dcubic1lem  26793  dcubic2  26794  dcubic  26796  mcubic  26797  cubic2  26798  dquartlem1  26801  dquart  26803  quart1lem  26805  quartlem1  26807  quart  26811  acoscos  26843  atanlogaddlem  26863  atantayl2  26888  atantayl3  26889  birthdaylem2  26902  efrlim  26919  efrlimOLD  26920  amgmlem  26940  logdifbnd  26944  emcllem3  26948  emcllem6  26951  lgamgulmlem2  26980  lgamgulmlem3  26981  lgamgulmlem4  26982  lgamgulmlem5  26983  gamigam  27003  lgamcvg2  27005  gamfac  27017  basellem3  27033  basellem8  27038  basellem9  27039  chtprm  27103  logfaclbnd  27173  perfect1  27179  bcp1ctr  27230  bclbnd  27231  bposlem1  27235  lgsdilem  27275  lgsdirnn0  27295  lgsdinn0  27296  gausslemma2dlem1a  27316  gausslemma2dlem4  27320  gausslemma2dlem5a  27321  lgseisenlem2  27327  lgsquadlem1  27331  2sqlem2  27369  mul2sq  27370  2sqmod  27387  2sqnn0  27389  vmadivsum  27433  rpvmasumlem  27438  dchrisumlem1  27440  dchrisumlem2  27441  dchrmusum2  27445  dchrvmasum2if  27448  dchrisum0lem2  27469  logsqvma2  27494  selberg3  27510  selberg4lem1  27511  pntrsumo1  27516  pntrlog2bndlem2  27529  pntrlog2bndlem3  27530  pntrlog2bndlem5  27532  pntibndlem2  27542  pntlemk  27557  pntlemo  27558  ostth2lem4  27587  ostth3  27589  subsfo  28045  negsval2  28046  ltonold  28241  noseqrdgfn  28286  n0fincut  28335  addhalfcut  28439  bdayfinbndlem1  28447  z12shalf  28460  tgbtwndiff  28562  tgifscgr  28564  trgcgrg  28571  motcgr3  28601  tgbtwnconn1lem1  28628  tgbtwnconn1lem2  28629  ismir  28715  miriso  28726  midexlem  28748  ragmir  28756  footexALT  28774  footexlem1  28775  footexlem2  28776  colperpexlem3  28788  mideulem2  28790  midex  28793  opphllem3  28805  midcgr  28836  lmiisolem  28852  brbtwn2  28962  colinearalglem4  28966  axsegconlem1  28974  axpaschlem  28997  axcontlem4  29024  axcontlem7  29027  axcontlem8  29028  ushgredgedgloop  29288  crctcshwlkn0lem6  29872  wwlknlsw  29904  wwlksnextwrd  29954  clwlkclwwlklem2a3  30053  clwlkclwwlk2  30062  clwwlkel  30105  clwwlkfo  30109  clwwlkext2edg  30115  eupth2eucrct  30276  numclwwlk2lem1lem  30401  numclwwlk1lem2fo  30417  numclwlk2lem2f  30436  grpoidinvlem2  30565  nvmtri  30731  cnnvm  30742  nvnd  30748  ipidsq  30770  ipnm  30771  ipipcj  30775  blocnilem  30864  ipasslem2  30892  dipsubdir  30908  hvaddsubval  31093  pjhthlem1  31451  pjspansn  31637  pjo  31731  unoplin  31980  adjadj  31996  hmoplin  32002  eigvec1  32022  lnopeqi  32068  nmcexi  32086  lnfnsubi  32106  riesz3i  32122  kbass6  32181  leoprf2  32187  leoprf  32188  pjnmopi  32208  mdslmd1lem1  32385  mdslmd1lem2  32386  superpos  32414  ifeq3da  32605  fresunsn  32687  fgreu  32733  cocnvf1o  32791  resf1o  32792  quad3d  32812  fprodex01  32889  sgnmul  32899  ccatws1f1o  33016  wrdt2ind  33018  mndlactfo  33092  mndractfo  33094  gsummpt2d  33115  gsummptp1  33123  xrge0tsmseq  33141  gsumwrd2dccatlem  33143  gsumwrd2dccat  33144  symgfcoeu  33148  wrdpmtrlast  33159  psgnfzto1stlem  33166  psgnfzto1st  33171  cycpm2tr  33185  cycpmco2lem6  33197  cycpmco2lem7  33198  subrgchr  33303  elrgspnlem1  33308  elrgspnlem3  33310  elrgspnsubrunlem1  33313  rloccring  33336  rhmdvd  33389  qusrn  33474  nsgqusf1olem3  33480  rhmquskerlem  33490  elrspunsn  33494  mxidlirredi  33536  qsdrngi  33560  1arithidomlem1  33600  1arithidomlem2  33601  evls1subd  33637  deg1prod  33648  r1pid2OLD  33674  evlextv  33691  psrmonprod  33701  esplyfval1  33722  esplyind  33724  esplyindfv  33725  esplyfvn  33726  vietalem  33728  resssra  33736  dimval  33750  dimvalfi  33751  lindsunlem  33774  dimkerim  33777  qusdimsum  33778  fedgmullem1  33779  extdg1id  33816  fldextrspunlsplem  33823  fldextrspunlsp  33824  fldextrspunlem1  33825  fldextrspundgdvds  33831  extdgfialglem1  33842  extdgfialglem2  33843  ply1annidllem  33851  algextdeglem4  33870  constrrtcc  33885  constrsslem  33891  constrresqrtcl  33927  cos9thpiminplylem2  33933  cos9thpiminply  33938  madjusmdetlem2  33978  qtophaus  33986  zarclssn  34023  zarcmplem  34031  pstmval  34045  mndpluscn  34076  qqhucn  34142  esumval  34196  gsumesum  34209  esumcst  34213  esumpcvgval  34228  oddpwdc  34504  eulerpartlemgvv  34526  probdif  34570  signsvtn  34734  actfunsnf1o  34754  reprpmtf1o  34776  hgt750lemd  34798  logdivsqrle  34800  hgt750lemg  34804  hgt750lemb  34806  bnj1415  35186  swrdrevpfx  35305  pfxwlk  35312  derangen2  35362  subfaclefac  35364  subfaclim  35376  satom  35544  fmla  35569  mrsubrn  35701  sinccvglem  35860  bcprod  35926  filnetlem4  36569  curunc  37914  ltflcei  37920  matunitlindflem1  37928  matunitlindflem2  37929  poimirlem16  37948  poimirlem17  37949  poimirlem19  37951  poimirlem20  37952  poimirlem24  37956  mblfinlem4  37972  ibladdnclem  37988  iblabsnc  37996  iblmulc2nc  37997  ftc1anclem6  38010  ftc1anclem8  38012  sdclem2  38054  ismtycnv  38114  heiborlem10  38132  lflvsass  39518  lkrscss  39535  eqlkr  39536  eqlkr3  39538  ldualvsdi2  39581  omllaw3  39682  cmtcomlemN  39685  cmtbr3N  39691  omlfh3N  39696  llnexchb2lem  40305  dalawlem7  40314  dalawlem11  40318  dalawlem12  40319  pol1N  40347  paddatclN  40386  4atexlemcnd  40509  ltrncoidN  40565  cdleme3b  40666  cdleme11  40707  cdleme15a  40711  cdleme22e  40781  cdleme22g  40785  cdlemg18b  41116  trlcoat  41160  cdlemk2  41269  cdlemk4  41271  cdlemki  41278  cdlemksv2  41284  cdlemk15  41292  cdlemk55a  41396  diainN  41494  dia2dimlem3  41503  dia2dimlem5  41505  dvhlveclem  41545  diaocN  41562  cdlemn4  41635  cdlemn8  41641  dihopelvalcpre  41685  dihmeetlem9N  41752  dih1dimatlem  41766  dihpN  41773  dochvalr3  41800  dochsat  41820  djhjlj  41840  dochdmm1  41847  dihjatcclem4  41858  dihjat1  41866  dihjat4  41870  dochsnkr2cl  41911  dochfl1  41913  lclkrlem2j  41953  mapdordlem2  42074  mapdrvallem2  42082  hdmap10  42277  lcmineqlem12  42471  3lexlogpow5ineq5  42491  aks4d1p1  42507  primrootsunit1  42528  primrootscoprmpow  42530  posbezout  42531  aks6d1c1p3  42541  aks6d1c1p4  42542  aks6d1c1p5  42543  aks6d1c1p7  42544  evl1gprodd  42548  hashscontpow1  42552  aks6d1c3  42554  aks6d1c2lem3  42557  aks6d1c2lem4  42558  aks6d1c2  42561  aks6d1c5lem3  42568  aks6d1c6lem1  42601  aks6d1c6isolem3  42607  aks6d1c6lem5  42608  bcle2d  42610  aks6d1c7lem1  42611  aks5lem3a  42620  grpods  42625  unitscyglem1  42626  unitscyglem2  42627  unitscyglem4  42629  unitscyglem5  42630  aks5lem7  42631  nicomachus  42743  sumcubes  42744  cnreeu  42934  frlmvscadiccat  42950  grpcominv1  42952  riccrng1  42965  ricdrng1  42972  frlmsnic  42984  evlselv  43019  fsuppind  43022  flt4lem7  43091  negexpidd  43113  3cubeslem2  43116  3cubeslem3r  43118  mzpsubmpt  43174  irrapxlem3  43255  pellexlem6  43265  pell1234qrne0  43284  pell1234qrreccl  43285  pell1234qrmulcl  43286  pell14qrdich  43300  pell1qrgaplem  43304  rmxluc  43367  rmyluc  43368  jm2.24nn  43390  jm2.18  43419  jm2.19lem2  43421  jm2.19lem3  43422  jm2.22  43426  jm2.23  43427  jm2.16nn0  43435  jm2.27c  43438  fnwe2lem2  43482  lmhmfgsplit  43517  hbtlem2  43555  onsucf1lem  43700  ofoafo  43787  naddcnffo  43795  naddwordnexlem4  43832  reabssgn  44066  relexpmulnn  44139  relexpmulg  44140  ntrclsneine0lem  44494  int-addassocd  44604  dvconstbi  44764  bccm1k  44772  binomcxplemnotnn0  44786  fmptsnxp  45602  wessf1ornlem  45618  projf1o  45629  infnsuprnmpt  45682  lefldiveq  45728  lt4addmuld  45742  fzdifsuc2  45746  suplesup  45772  infrpge  45784  xrlexaddrp  45785  xralrple2  45787  infleinflem1  45802  supminfrnmpt  45877  supminfxr2  45901  fsumnncl  46006  limcperiod  46062  sumnnodd  46064  limcresiooub  46074  limcresioolb  46075  0ellimcdiv  46081  reclimc  46085  limsupval3  46124  limsupequzmpt2  46150  liminfval5  46197  limsupresxr  46198  liminfresxr  46199  liminfvalxr  46215  liminfequzmpt2  46223  climliminflimsupd  46233  liminfltlem  46236  liminflbuz2  46247  sinmulcos  46297  coskpi2  46298  cncfdmsn  46322  cncfiooicclem1  46325  fprodsubrecnncnvlem  46339  fprodaddrecnncnvlem  46341  fperdvper  46351  dvnmptdivc  46370  dvnxpaek  46374  dvnmul  46375  dvnprodlem1  46378  dvnprodlem3  46380  itgcoscmulx  46401  itgsincmulx  46406  itgspltprt  46411  itgiccshift  46412  itgperiod  46413  sublevolico  46416  volioof  46419  ovolsplit  46420  fvvolioof  46421  fvvolicof  46423  stoweidlem22  46454  stoweidlem32  46464  wallispilem5  46501  stirlinglem5  46510  dirkertrigeqlem2  46531  dirkertrigeq  46533  dirkercncflem1  46535  dirkercncflem2  46536  dirkercncflem4  46538  fourierdlem13  46552  fourierdlem16  46555  fourierdlem19  46558  fourierdlem21  46560  fourierdlem22  46561  fourierdlem28  46567  fourierdlem32  46571  fourierdlem33  46572  fourierdlem42  46581  fourierdlem47  46585  fourierdlem48  46586  fourierdlem49  46587  fourierdlem50  46588  fourierdlem56  46594  fourierdlem60  46598  fourierdlem61  46599  fourierdlem64  46602  fourierdlem66  46604  fourierdlem71  46609  fourierdlem73  46611  fourierdlem74  46612  fourierdlem76  46614  fourierdlem78  46616  fourierdlem79  46617  fourierdlem80  46618  fourierdlem81  46619  fourierdlem83  46621  fourierdlem88  46626  fourierdlem92  46630  fourierdlem93  46631  fourierdlem97  46635  fourierdlem101  46639  fourierdlem103  46641  fourierdlem104  46642  fourierdlem109  46647  fourierdlem111  46649  fouriersw  46663  elaa2lem  46665  etransclem24  46690  etransclem25  46691  etransclem35  46701  etransclem46  46712  rrndistlt  46722  rrxunitopnfi  46724  qndenserrnbl  46727  qndenserrnopnlem  46729  saldifcl2  46760  intsal  46762  sge0sn  46811  sge0ltfirp  46832  sge0iunmptlemre  46847  sge0fodjrnlem  46848  sge0isum  46859  sge0xaddlem1  46865  nnfoctbdjlem  46887  meassle  46895  ismeannd  46899  meadif  46911  meaiuninclem  46912  meaiininclem  46918  omeunile  46937  caragendifcl  46946  caratheodory  46960  isomenndlem  46962  ovnsubaddlem1  47002  hoidmv1lelem2  47024  hoidmv1le  47026  hoidmvlelem2  47028  hoidmvle  47032  hoi2toco  47039  rrnmbl  47046  hoidifhspdmvle  47052  voncmpl  47053  hoiqssbl  47057  hspmbllem1  47058  hspmbllem2  47059  ovolval2lem  47075  ovolval5lem2  47085  ovnovollem1  47088  ovnovollem2  47089  hoimbl2  47097  vonhoire  47104  salpreimagelt  47139  salpreimalegt  47141  preimaioomnf  47151  smfres  47222  smfmullem1  47223  smflimmpt  47242  smfsupmpt  47247  smfinfmpt  47251  smflimsupmpt  47261  smfliminflem  47262  smfliminfmpt  47264  sigarcol  47296  f1oresf1o  47724  elsprel  47909  prproropf1o  47941  paireqne  47945  sfprmdvdsmersenne  48037  lighneallem3  48041  lighneallem4  48044  nn0onn0exALTV  48133  nnsum3primesprm  48224  nnsum4primesodd  48230  nnsum4primesoddALTV  48231  isuspgrim0lem  48327  clnbgrgrimlem  48367  uspgrlimlem3  48424  uspgrlimlem4  48425  gpgedgvtx0  48495  gpgedgvtx1  48496  funcringcsetcALTV2lem7  48730  funcringcsetclem7ALTV  48753  lincext3  48890  lincresunit3  48915  nn0onn0ex  48957  nnpw2pmod  49017  blennn0em1  49025  digexp  49041  dignn0ehalf  49051  nn0mulfsum  49058  itcovalpclem1  49104  eenglngeehlnmlem2  49172  rrx2vlinest  49175  line2  49186  itschlc0xyqsol  49201  itsclinecirc0b  49208  toplatjoin  49435  toplatmeet  49436  upeu2lem  49461  oppff1o  49582  imaf1co  49588  upciclem3  49601  natoppfb  49664  oppcthinco  49872  oppcthinendcALT  49874  lmddu  50100  recsec  50189  reccsc  50190  aacllem  50234  amgmlemALT  50236