Theorem eqtr2d 2767

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

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2718

This theorem is referenced by:  3eqtrrd  2771  3eqtr2rd  2773  ifan  4576  ifor  4577  dfopif  4865  fnco  6661  fnsnfv  6964  nvocnv  7275  elovmpt3rab1  7663  onsucmin  7806  csbopeq1a  8035  oaabs2  8650  ecinxp  8788  fsetfocdm  8857  resixpfo  8932  sbthlem3  9087  rankxpsuc  9879  fseqenlem2  10022  dfac2b  10127  isf32lem9  10358  compsscnvlem  10367  ttukeylem7  10512  fpwwe2lem10  10637  00id  11393  submul2  11658  mulsubfacd  11679  divadddiv  11933  infrenegsup  12201  xadd4d  13288  fzdifsuc  13567  fzval3  13707  fzoshftral  13755  ceim1l  13818  fldiv  13831  flmod  13856  intfrac  13857  modcyc2  13878  moddi  13910  uzrdgfni  13929  axdc4uzlem  13954  seqf1olem1  14012  seqf1olem2  14013  seqid2  14019  expnegz  14067  binom2sub  14188  binom3  14192  hashreshashfun  14404  ccatw2s1p2  14593  ccats1pfxeq  14670  pfxccatin12lem2  14687  pfxccatin12  14689  swrdccat3b  14696  cshweqrep  14777  2cshwcshw  14782  ccatco  14792  swrds2  14897  relexpsucnnr  14978  relexpaddnn  15004  reim  15062  mulre  15074  addcj  15101  absimle  15262  clim2ser  15607  isercoll2  15621  serf0  15633  iseralt  15637  summolem3  15666  isumclim3  15711  mptfzshft  15730  fsumrev  15731  fsum2mul  15741  incexc  15789  isumsplit  15792  mertenslem1  15836  fprodrev  15927  iprodclim3  15950  binomfallfaclem2  15990  ef4p  16063  tanval3  16084  efival  16102  sinmul  16122  bitsinvp1  16397  sadaddlem  16414  bitsshft  16423  smu01lem  16433  dfgcd2  16495  lcmgcdlem  16550  lcm1  16554  lcmfass  16590  eulerthlem2  16724  hashgcdeq  16731  powm2modprm  16745  pythagtriplem16  16772  pczpre  16789  pcqdiv  16799  pcadd  16831  pcfac  16841  prmreclem5  16862  4sqlem10  16889  4sqlem19  16905  vdwapun  16916  vdwlem1  16923  ramcl  16971  setsstruct  17118  strfvd  17143  strfv2d  17144  xpsff1o  17522  xpsrnbas  17526  2oppccomf  17680  oppcepi  17695  sscfn1  17773  sscfn2  17774  invfuc  17939  funcestrcsetclem7  18110  funcsetcestrclem7  18125  gsumsplit1r  18620  grpinvssd  18945  grpinvval2  18951  cycsubggend  19131  pmtrdifwrdellem2  19402  psgnunilem1  19413  psgnuni  19419  pgp0  19516  sylow1lem1  19518  sylow3lem2  19548  efgredleme  19663  efgcpbllemb  19675  frgpuptinv  19691  frgpup3lem  19697  gexexlem  19772  cyggenod  19804  gsumval3eu  19824  gsumval3  19827  gsumzaddlem  19841  dprd2db  19965  ablsimpgfindlem1  20029  ringinvdv  20316  c0snmgmhm  20364  rngcifuestrc  20535  funcrngcsetc  20536  funcrngcsetcALT  20537  funcringcsetc  20570  lss1d  20810  pwssplit1  20907  rngqiprnglin  21155  znzrh2  21440  regsumsupp  21515  ipassr2  21540  dsmmfi  21633  frlmlss  21646  frlmip  21673  frlmlbs  21692  frlmup3  21695  islindf4  21733  mplcoe3  21935  subrgascl  21969  evlseu  21988  psdadd  22046  ply1sclid  22162  ply1chr  22180  1marepvmarrepid  22432  madurid  22501  smadiadetlem3  22525  mat2pmatghm  22587  pmatcollpwscmatlem1  22646  pm2mpmhmlem2  22676  cpmadurid  22724  cpmidgsumm2pm  22726  cpmadugsumlemB  22731  cayhamlem2  22741  ntrval2  22910  ordtuni  23049  cnclima  23127  cmpsub  23259  ptbasfi  23440  txbasval  23465  pt1hmeo  23665  alexsubALTlem1  23906  trust  24089  ussid  24120  ressuss  24122  ressprdsds  24232  imasdsf1olem  24234  setsms  24343  tmsxms  24350  tmsxpsmopn  24401  subgnm  24497  tngnm  24523  tngngp2  24524  xrsxmet  24680  xrge0gsumle  24704  metdstri  24722  xrhmeo  24826  lebnumlem3  24844  pcorevlem  24908  pi1xfrcnvlem  24938  clmabs  24965  cvsmuleqdivd  25016  rrxip  25273  rrxds  25276  rrxdsfi  25294  minveclem4a  25313  pjthlem1  25320  divcncf  25331  ovolunlem1a  25380  mbfres2  25529  i1faddlem  25577  ibladdlem  25704  iblabs  25713  ditgsplit  25745  dvmptresicc  25800  dvnres  25816  dvmptdiv  25861  dveflem  25866  dveq0  25888  dvfsumabs  25912  itgsubstlem  25938  ply1divex  26027  dgrco  26165  plycjlem  26166  taylthlem1  26263  pserdv2  26322  abelthlem6  26328  abelthlem7  26330  tangtx  26395  abssinper  26410  sineq0  26413  explog  26483  reexplog  26484  eflogeq  26491  abslogle  26507  tanarg  26508  logtayl  26549  logtayl2  26551  relogbdiv  26666  ang180lem3  26698  affineequiv  26710  affineequiv2  26711  chordthmlem4  26722  chordthmlem5  26723  heron  26725  dcubic1lem  26730  dcubic2  26731  dcubic  26733  mcubic  26734  cubic2  26735  dquartlem1  26738  dquart  26740  quart1lem  26742  quartlem1  26744  quart  26748  acoscos  26780  atanlogaddlem  26800  atantayl2  26825  atantayl3  26826  birthdaylem2  26839  efrlim  26856  efrlimOLD  26857  amgmlem  26877  logdifbnd  26881  emcllem3  26885  emcllem6  26888  lgamgulmlem2  26917  lgamgulmlem3  26918  lgamgulmlem4  26919  lgamgulmlem5  26920  gamigam  26940  lgamcvg2  26942  gamfac  26954  basellem3  26970  basellem8  26975  basellem9  26976  chtprm  27040  logfaclbnd  27110  perfect1  27116  bcp1ctr  27167  bclbnd  27168  bposlem1  27172  lgsdilem  27212  lgsdirnn0  27232  lgsdinn0  27233  gausslemma2dlem1a  27253  gausslemma2dlem4  27257  gausslemma2dlem5a  27258  lgseisenlem2  27264  lgsquadlem1  27268  2sqlem2  27306  mul2sq  27307  2sqmod  27324  2sqnn0  27326  vmadivsum  27370  rpvmasumlem  27375  dchrisumlem1  27377  dchrisumlem2  27378  dchrmusum2  27382  dchrvmasum2if  27385  dchrisum0lem2  27406  logsqvma2  27431  selberg3  27447  selberg4lem1  27448  pntrsumo1  27453  pntrlog2bndlem2  27466  pntrlog2bndlem3  27467  pntrlog2bndlem5  27469  pntibndlem2  27479  pntlemk  27494  pntlemo  27495  ostth2lem4  27524  ostth3  27526  negsval2  27929  sltonold  28108  noseqrdgfn  28134  tgbtwndiff  28265  tgifscgr  28267  trgcgrg  28274  motcgr3  28304  tgbtwnconn1lem1  28331  tgbtwnconn1lem2  28332  ismir  28418  miriso  28429  midexlem  28451  ragmir  28459  footexALT  28477  footexlem1  28478  footexlem2  28479  colperpexlem3  28491  mideulem2  28493  midex  28496  opphllem3  28508  midcgr  28539  lmiisolem  28555  brbtwn2  28671  colinearalglem4  28675  axsegconlem1  28683  axpaschlem  28706  axcontlem4  28733  axcontlem7  28736  axcontlem8  28737  ushgredgedgloop  28996  crctcshwlkn0lem6  29578  wwlknlsw  29610  wwlksnextwrd  29660  clwlkclwwlklem2a3  29756  clwlkclwwlk2  29765  clwwlkel  29808  clwwlkfo  29812  clwwlkext2edg  29818  eupth2eucrct  29979  numclwwlk2lem1lem  30104  numclwwlk1lem2fo  30120  numclwlk2lem2f  30139  grpoidinvlem2  30267  nvmtri  30433  cnnvm  30444  nvnd  30450  ipidsq  30472  ipnm  30473  ipipcj  30477  blocnilem  30566  ipasslem2  30594  dipsubdir  30610  hvaddsubval  30795  pjhthlem1  31153  pjspansn  31339  pjo  31433  unoplin  31682  adjadj  31698  hmoplin  31704  eigvec1  31724  lnopeqi  31770  nmcexi  31788  lnfnsubi  31808  riesz3i  31824  kbass6  31883  leoprf2  31889  leoprf  31890  pjnmopi  31910  mdslmd1lem1  32087  mdslmd1lem2  32088  superpos  32116  ifeq3da  32287  fgreu  32406  resf1o  32462  fprodex01  32536  wrdt2ind  32622  gsummpt2d  32707  xrge0tsmseq  32717  symgfcoeu  32749  psgnfzto1stlem  32765  psgnfzto1st  32770  cycpm2tr  32784  cycpmco2lem6  32796  cycpmco2lem7  32797  subrgchr  32888  rhmdvd  32939  qusrn  33026  nsgqusf1olem3  33032  rhmquskerlem  33049  elrspunsn  33053  mxidlirredi  33093  qsdrngi  33115  evls1addd  33157  evls1subd  33158  evls1muld  33159  evls1vsca  33160  r1pid2  33184  resssra  33192  dimval  33203  dimvalfi  33204  lindsunlem  33227  dimkerim  33230  qusdimsum  33231  fedgmullem1  33232  extdg1id  33260  evls1maprhm  33278  evls1maplmhm  33279  evls1maprnss  33280  ply1annidllem  33281  algextdeglem4  33297  madjusmdetlem2  33338  qtophaus  33346  zarclssn  33383  zarcmplem  33391  pstmval  33405  mndpluscn  33436  qqhucn  33502  esumval  33574  gsumesum  33587  esumcst  33591  esumpcvgval  33606  oddpwdc  33883  eulerpartlemgvv  33905  probdif  33949  sgnmul  34071  signsvtn  34125  actfunsnf1o  34145  reprpmtf1o  34167  hgt750lemd  34189  logdivsqrle  34191  hgt750lemg  34195  hgt750lemb  34197  bnj1415  34578  swrdrevpfx  34635  pfxwlk  34642  derangen2  34693  subfaclefac  34695  subfaclim  34707  satom  34875  fmla  34900  mrsubrn  35032  sinccvglem  35185  bcprod  35241  filnetlem4  35774  curunc  36983  ltflcei  36989  matunitlindflem1  36997  matunitlindflem2  36998  poimirlem16  37017  poimirlem17  37018  poimirlem19  37020  poimirlem20  37021  poimirlem24  37025  mblfinlem4  37041  ibladdnclem  37057  iblabsnc  37065  iblmulc2nc  37066  ftc1anclem6  37079  ftc1anclem8  37081  sdclem2  37123  ismtycnv  37183  heiborlem10  37201  lflvsass  38464  lkrscss  38481  eqlkr  38482  eqlkr3  38484  ldualvsdi2  38527  omllaw3  38628  cmtcomlemN  38631  cmtbr3N  38637  omlfh3N  38642  llnexchb2lem  39252  dalawlem7  39261  dalawlem11  39265  dalawlem12  39266  pol1N  39294  paddatclN  39333  4atexlemcnd  39456  ltrncoidN  39512  cdleme3b  39613  cdleme11  39654  cdleme15a  39658  cdleme22e  39728  cdleme22g  39732  cdlemg18b  40063  trlcoat  40107  cdlemk2  40216  cdlemk4  40218  cdlemki  40225  cdlemksv2  40231  cdlemk15  40239  cdlemk55a  40343  diainN  40441  dia2dimlem3  40450  dia2dimlem5  40452  dvhlveclem  40492  diaocN  40509  cdlemn4  40582  cdlemn8  40588  dihopelvalcpre  40632  dihmeetlem9N  40699  dih1dimatlem  40713  dihpN  40720  dochvalr3  40747  dochsat  40767  djhjlj  40787  dochdmm1  40794  dihjatcclem4  40805  dihjat1  40813  dihjat4  40817  dochsnkr2cl  40858  dochfl1  40860  lclkrlem2j  40900  mapdordlem2  41021  mapdrvallem2  41029  hdmap10  41224  lcmineqlem12  41422  3lexlogpow5ineq5  41442  aks4d1p1  41458  primrootsunit1  41478  primrootscoprmpow  41480  posbezout  41481  aks6d1c1p3  41488  aks6d1c1p4  41489  aks6d1c1p5  41490  aks6d1c1p7  41491  evl1gprodd  41495  hashscontpow1  41499  aks6d1c3  41501  aks6d1c2lem3  41503  aks6d1c2lem4  41504  aks6d1c2  41507  aks6d1c5lem3  41514  aks6d1c6lem1  41548  frlmvscadiccat  41646  grpcominv1  41648  riccrng1  41660  ricdrng1  41666  frlmsnic  41672  evlselv  41721  fsuppind  41724  nicomachus  41773  sumcubes  41774  cnreeu  41924  flt4lem7  41984  negexpidd  42003  3cubeslem2  42006  3cubeslem3r  42008  mzpsubmpt  42064  irrapxlem3  42145  pellexlem6  42155  pell1234qrne0  42174  pell1234qrreccl  42175  pell1234qrmulcl  42176  pell14qrdich  42190  pell1qrgaplem  42194  rmxluc  42258  rmyluc  42259  jm2.24nn  42281  jm2.18  42310  jm2.19lem2  42312  jm2.19lem3  42313  jm2.22  42317  jm2.23  42318  jm2.16nn0  42326  jm2.27c  42329  fnwe2lem2  42376  lmhmfgsplit  42411  hbtlem2  42449  onsucf1lem  42600  ofoafo  42687  naddcnffo  42695  naddwordnexlem4  42733  reabssgn  42968  relexpmulnn  43041  relexpmulg  43042  ntrclsneine0lem  43396  int-addassocd  43507  dvconstbi  43674  bccm1k  43682  binomcxplemnotnn0  43696  fmptsnxp  44445  wessf1ornlem  44461  projf1o  44473  infnsuprnmpt  44531  lefldiveq  44579  lt4addmuld  44593  fzdifsuc2  44597  suplesup  44626  infrpge  44638  xrlexaddrp  44639  xralrple2  44641  infleinflem1  44657  supminfrnmpt  44732  supminfxr2  44756  fsumnncl  44865  limcperiod  44921  sumnnodd  44923  limcresiooub  44935  limcresioolb  44936  0ellimcdiv  44942  reclimc  44946  limsupval3  44985  limsupequzmpt2  45011  liminfval5  45058  limsupresxr  45059  liminfresxr  45060  liminfvalxr  45076  liminfequzmpt2  45084  climliminflimsupd  45094  liminfltlem  45097  liminflbuz2  45108  sinmulcos  45158  coskpi2  45159  cncfdmsn  45183  cncfiooicclem1  45186  fprodsubrecnncnvlem  45200  fprodaddrecnncnvlem  45202  fperdvper  45212  dvnmptdivc  45231  dvnxpaek  45235  dvnmul  45236  dvnprodlem1  45239  dvnprodlem3  45241  itgcoscmulx  45262  itgsincmulx  45267  itgspltprt  45272  itgiccshift  45273  itgperiod  45274  sublevolico  45277  volioof  45280  ovolsplit  45281  fvvolioof  45282  fvvolicof  45284  stoweidlem22  45315  stoweidlem32  45325  wallispilem5  45362  stirlinglem5  45371  dirkertrigeqlem2  45392  dirkertrigeq  45394  dirkercncflem1  45396  dirkercncflem2  45397  dirkercncflem4  45399  fourierdlem13  45413  fourierdlem16  45416  fourierdlem19  45419  fourierdlem21  45421  fourierdlem22  45422  fourierdlem28  45428  fourierdlem32  45432  fourierdlem33  45433  fourierdlem42  45442  fourierdlem47  45446  fourierdlem48  45447  fourierdlem49  45448  fourierdlem50  45449  fourierdlem56  45455  fourierdlem60  45459  fourierdlem61  45460  fourierdlem64  45463  fourierdlem66  45465  fourierdlem71  45470  fourierdlem73  45472  fourierdlem74  45473  fourierdlem76  45475  fourierdlem78  45477  fourierdlem79  45478  fourierdlem80  45479  fourierdlem81  45480  fourierdlem83  45482  fourierdlem88  45487  fourierdlem92  45491  fourierdlem93  45492  fourierdlem97  45496  fourierdlem101  45500  fourierdlem103  45502  fourierdlem104  45503  fourierdlem109  45508  fourierdlem111  45510  fouriersw  45524  elaa2lem  45526  etransclem24  45551  etransclem25  45552  etransclem35  45562  etransclem46  45573  rrndistlt  45583  rrxunitopnfi  45585  qndenserrnbl  45588  qndenserrnopnlem  45590  saldifcl2  45621  intsal  45623  sge0sn  45672  sge0ltfirp  45693  sge0iunmptlemre  45708  sge0fodjrnlem  45709  sge0isum  45720  sge0xaddlem1  45726  nnfoctbdjlem  45748  meassle  45756  ismeannd  45760  meadif  45772  meaiuninclem  45773  meaiininclem  45779  omeunile  45798  caragendifcl  45807  caratheodory  45821  isomenndlem  45823  ovnsubaddlem1  45863  hoidmv1lelem2  45885  hoidmv1le  45887  hoidmvlelem2  45889  hoidmvle  45893  hoi2toco  45900  rrnmbl  45907  hoidifhspdmvle  45913  voncmpl  45914  hoiqssbl  45918  hspmbllem1  45919  hspmbllem2  45920  ovolval2lem  45936  ovolval5lem2  45946  ovnovollem1  45949  ovnovollem2  45950  hoimbl2  45958  vonhoire  45965  salpreimagelt  46000  salpreimalegt  46002  preimaioomnf  46012  smfres  46083  smfmullem1  46084  smflimmpt  46103  smfsupmpt  46108  smfinfmpt  46112  smflimsupmpt  46122  smfliminflem  46123  smfliminfmpt  46125  sigarcol  46157  f1oresf1o  46575  elsprel  46720  prproropf1o  46752  paireqne  46756  sfprmdvdsmersenne  46848  lighneallem3  46852  lighneallem4  46855  nn0onn0exALTV  46944  nnsum3primesprm  47035  nnsum4primesodd  47041  nnsum4primesoddALTV  47042  funcringcsetcALTV2lem7  47251  funcringcsetclem7ALTV  47274  lincext3  47417  lincresunit3  47442  nn0onn0ex  47489  nnpw2pmod  47549  blennn0em1  47557  digexp  47573  dignn0ehalf  47583  nn0mulfsum  47590  itcovalpclem1  47636  eenglngeehlnmlem2  47704  rrx2vlinest  47707  line2  47718  itschlc0xyqsol  47733  itsclinecirc0b  47740  toplatjoin  47906  toplatmeet  47907  recsec  48080  reccsc  48081  aacllem  48127  amgmlemALT  48129