Theorem eqtr2d 2799

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  3eqtrrd  2803  3eqtr2rd  2805  ifan  4539  ifor  4540  dfopif  4842  fnco  6687  fnsnfv  6995  nvocnv  7320  elovmpt3rab1  7713  onsucmin  7866  csbopeq1a  8096  fnwe2lem3  8184  oaabs2  8696  ecinxp  8851  resixpfo  9002  sbthlem3  9146  rankxpsuc  9936  fseqenlem2  10143  dfac2b  10248  isf32lem9  10478  compsscnvlem  10487  ttukeylem7  10632  fpwwe2lem10  10764  00id  11524  submul2  11795  mulsubfacd  11817  divadddiv  12072  infrenegsup  12340  xadd4d  13473  fzdifsuc  13758  fzval3  13909  fzoshftral  13962  ceim1l  14027  fldiv  14040  flmod  14065  intfrac  14066  modcyc2  14087  modaddb  14089  moddi  14122  uzrdgfni  14141  axdc4uzlem  14166  seqf1olem1  14224  seqf1olem2  14225  seqid2  14231  expnegz  14279  addmuldir2d  14396  binom2sub  14405  binom3  14409  hashreshashfun  14625  ccatw2s1p2  14827  ccats1pfxeq  14905  pfxccatin12lem2  14922  pfxccatin12  14924  swrdccat3b  14931  swrdrevpfx  14960  cshweqrep  15014  2cshwcshw  15018  ccatco  15028  swrds2  15134  relexpsucnnr  15221  relexpaddnn  15247  sgnmul  15303  reim  15319  mulre  15331  addcj  15358  absimle  15519  clim2ser  15866  isercoll2  15880  serf0  15892  iseralt  15896  summolem3  15924  isumclim3  15969  mptfzshft  15988  fsumrev  15989  fsum2mul  15999  incexc  16050  isumsplit  16053  mertenslem1  16097  fprodrev  16188  iprodclim3  16211  binomfallfaclem2  16250  ef4p  16325  tanval3  16346  efival  16364  sinmul  16384  bitsinvp1  16663  sadaddlem  16680  bitsshft  16689  smu01lem  16699  dfgcd2  16763  lcmgcdlem  16825  lcm1  16829  lcmfass  16865  eulerthlem2  17003  hashgcdeq  17011  powm2modprm  17025  pythagtriplem16  17052  pczpre  17069  pcqdiv  17079  pcadd  17111  pcfac  17121  prmreclem5  17142  4sqlem10  17169  4sqlem19  17185  vdwapun  17196  vdwlem1  17203  ramcl  17251  setsstruct  17398  strfvd  17422  strfv2d  17423  xpsff1o  17789  xpsrnbas  17793  2oppccomf  17949  oppcepi  17964  sscfn1  18042  sscfn2  18043  invfuc  18202  funcestrcsetclem7  18370  funcsetcestrclem7  18385  gsumsplit1r  18926  grpinvssd  19277  grpinvval2  19283  cycsubggend  19470  pmtrdifwrdellem2  19747  psgnunilem1  19758  psgnuni  19764  pgp0  19861  sylow1lem1  19863  sylow3lem2  19893  efgredleme  20008  efgcpbllemb  20020  frgpuptinv  20036  frgpup3lem  20042  gexexlem  20117  cyggenod  20149  gsumval3eu  20169  gsumval3  20172  gsumzaddlem  20186  dprd2db  20310  ablsimpgfindlem1  20374  ringinvdv  20695  c0snmgmhm  20743  rngcifuestrc  20942  funcrngcsetc  20943  funcrngcsetcALT  20944  funcringcsetc  20977  lss1d  21289  pwssplit1  21385  rhmqusnsg  21632  rngqiprnglin  21649  znzrh2  21906  regsumsupp  21983  ipassr2  22008  dsmmfi  22099  frlmlss  22112  frlmip  22139  frlmlbs  22158  frlmup3  22161  islindf4  22199  mplcoe3  22402  subrgascl  22430  evlseu  22447  psdadd  22539  ply1sclid  22662  ply1chr  22679  evls1addd  22744  evls1muld  22745  evls1vsca  22746  evls1maprhm  22749  evls1maplmhm  22750  evls1maprnss  22751  evl1maprhm  22752  1marepvmarrepid  22945  madurid  23014  smadiadetlem3  23038  matunitlindflem1  23049  matunitlindflem2  23050  mat2pmatghm  23103  pmatcollpwscmatlem1  23162  pm2mpmhmlem2  23192  cpmadurid  23240  cpmidgsumm2pm  23242  cpmadugsumlemB  23247  cayhamlem2  23257  ntrval2  23424  ordtuni  23563  cnclima  23641  cmpsub  23773  ptbasfi  23955  txbasval  23980  pt1hmeo  24180  alexsubALTlem1  24421  trust  24603  ussid  24634  ressuss  24636  ressprdsds  24745  imasdsf1olem  24747  setsms  24854  tmsxms  24860  tmsxpsmopn  24911  subgnm  25007  tngnm  25025  tngngp2  25026  xrsxmet  25184  xrge0gsumle  25208  metdstri  25226  xrhmeo  25322  lebnumlem3  25339  pcorevlem  25402  pi1xfrcnvlem  25432  clmabs  25459  cvsmuleqdivd  25510  rrxip  25766  rrxds  25769  rrxdsfi  25787  minveclem4a  25806  pjthlem1  25813  divcncf  25823  ovolunlem1a  25872  mbfres2  26021  i1faddlem  26069  ibladdlem  26195  iblabs  26204  ditgsplit  26236  dvmptresicc  26291  dvnres  26306  dvmptdiv  26349  dveflem  26354  dveq0  26375  dvfsumabs  26398  itgsubstlem  26423  ply1divex  26510  r1pid2  26535  dgrco  26649  plycjlem  26650  taylthlem1  26757  pserdv2  26814  abelthlem6  26820  abelthlem7  26822  tangtx  26891  abssinper  26906  sineq0  26909  explog  26979  reexplog  26980  eflogeq  26987  abslogle  27003  tanarg  27004  logtayl  27045  logtayl2  27047  relogbdiv  27164  ang180lem3  27196  affineequiv  27208  affineequiv2  27209  chordthmlem4  27220  chordthmlem5  27221  heron  27223  dcubic1lem  27228  dcubic2  27229  dcubic  27231  mcubic  27232  cubic2  27233  dquartlem1  27236  dquart  27238  quart1lem  27240  quartlem1  27242  quart  27246  acoscos  27278  atanlogaddlem  27298  atantayl2  27323  atantayl3  27324  birthdaylem2  27337  efrlim  27354  amgmlem  27374  logdifbnd  27378  emcllem3  27382  emcllem6  27385  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamgulmlem4  27416  lgamgulmlem5  27417  gamigam  27437  lgamcvg2  27439  gamfac  27451  basellem3  27467  basellem8  27472  basellem9  27473  chtprm  27537  logfaclbnd  27606  perfect1  27612  bcp1ctr  27663  bclbnd  27664  bposlem1  27668  lgsdilem  27708  lgsdirnn0  27728  lgsdinn0  27729  gausslemma2dlem1a  27749  gausslemma2dlem4  27753  gausslemma2dlem5a  27754  lgseisenlem2  27760  lgsquadlem1  27764  2sqlem2  27802  mul2sq  27803  2sqmod  27820  2sqnn0  27822  vmadivsum  27866  rpvmasumlem  27871  dchrisumlem1  27873  dchrisumlem2  27874  dchrmusum2  27878  dchrvmasum2if  27881  dchrisum0lem2  27902  logsqvma2  27927  selberg3  27943  selberg4lem1  27944  pntrsumo1  27949  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem5  27965  pntibndlem2  27975  pntlemk  27990  pntlemo  27991  ostth2lem4  28020  ostth3  28022  flt4lem7  28046  subsfo  28508  negsval2  28509  ltonold  28704  noseqrdgfn  28749  n0fincut  28798  addhalfcut  28902  bdayfinbndlem1  28910  z12shalf  28923  tgbtwndiff  29026  tgifscgr  29028  trgcgrg  29035  motcgr3  29065  tgbtwnconn1lem1  29092  tgbtwnconn1lem2  29093  ismir  29188  miriso  29199  midexlem  29221  symquadprlnglem  29222  ragmir  29232  footexALT  29250  footexlem1  29251  footexlem2  29252  colperpexlem3  29265  mideulem2  29267  midex  29270  opphllem3  29282  midcgr  29342  lmiisolem  29358  prlngmid2  29496  quadcgrprlng  29501  brbtwn2  29540  colinearalglem4  29544  axsegconlem1  29552  axpaschlem  29575  axcontlem4  29602  axcontlem7  29605  axcontlem8  29606  ushgredgedgloop  29869  pfxwlk  30323  crctcshwlkn0lem6  30461  wwlknlsw  30493  wwlksnextwrd  30543  clwlkclwwlklem2a3  30642  clwlkclwwlk2  30651  clwwlkel  30694  clwwlkfo  30698  clwwlkext2edg  30704  eupth2eucrct  30875  numclwwlk2lem1lem  31000  numclwwlk1lem2fo  31016  numclwlk2lem2f  31035  grpoidinvlem2  31164  nvmtri  31330  cnnvm  31341  nvnd  31347  ipidsq  31369  ipnm  31370  ipipcj  31374  blocnilem  31463  ipasslem2  31491  dipsubdir  31507  hvaddsubval  31692  pjhthlem1  32050  pjspansn  32236  pjo  32330  unoplin  32579  adjadj  32595  hmoplin  32601  eigvec1  32621  lnopeqi  32667  nmcexi  32685  lnfnsubi  32705  riesz3i  32721  kbass6  32780  leoprf2  32786  leoprf  32787  pjnmopi  32807  mdslmd1lem1  32984  mdslmd1lem2  32985  superpos  33013  ifeq3da  33240  fgreu  33363  cocnvf1o  33417  resf1o  33418  quad3d  33437  fprodex01  33512  ccatws1f1o  33610  wrdt2ind  33612  mndlactfo  33687  mndractfo  33689  gsummpt2d  33709  gsummptp1  33717  xrge0tsmseq  33735  gsumwrd2dccatlem  33737  gsumwrd2dccat  33738  symgfcoeu  33742  wrdpmtrlast  33753  psgnfzto1stlem  33760  psgnfzto1st  33765  cycpm2tr  33779  cycpmco2lem6  33791  cycpmco2lem7  33792  subrgchr  33896  elrgspnlem1  33902  elrgspnlem3  33904  elrgspnsubrunlem1  33907  rloccring  33931  edompidlem  33960  rhmdvd  33989  qusrn  34064  nsgqusf1olem3  34070  rhmquskerlem  34079  elrspunsn  34083  mxidlirredi  34100  qsdrngi  34123  1arithidomlem1  34171  1arithidomlem2  34172  evls1subd  34207  deg1prod  34218  evls1degle1  34239  0mplrim  34257  evlextv  34285  psrmonprod  34295  esplyfval1  34316  esplyind  34318  esplyindfv  34319  esplyfvn  34320  vietalem  34322  resssra  34330  dimval  34344  dimvalfi  34345  lindsunlem  34367  dimkerim  34370  qusdimsum  34371  fedgmullem1  34372  extdg1id  34409  fldextrspunlsplem  34416  fldextrspunlsp  34417  fldextrspunlem1  34418  fldextrspundgdvds  34424  extdgfialglem1  34435  extdgfialglem2  34436  ply1annidllem  34444  algextdeglem4  34463  constrrtcc  34478  constrsslem  34484  constrresqrtcl  34520  cos9thpiminplylem2  34526  cos9thpiminply  34531  madjusmdetlem2  34571  qtophaus  34579  zarclssn  34616  zarcmplem  34624  pstmval  34638  mndpluscn  34669  qqhucn  34735  esumval  34789  gsumesum  34802  esumcst  34806  esumpcvgval  34821  oddpwdc  35097  eulerpartlemgvv  35119  probdif  35163  signsvtn  35324  actfunsnf1o  35344  reprpmtf1o  35366  hgt750lemd  35388  logdivsqrle  35390  hgt750lemg  35394  hgt750lemb  35396  bnj1415  35779  gdlopcfv2  36014  vonf1oonfo  36090  derangen2  36147  subfaclefac  36149  subfaclim  36161  satom  36329  fmla  36354  mrsubrn  36486  sinccvglem  36645  bcprod  36718  nmulss1  37178  filnetlem4  37384  curunc  38793  ltflcei  38799  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem24  38830  mblfinlem4  38846  ibladdnclem  38862  iblabsnc  38870  iblmulc2nc  38871  ftc1anclem6  38884  ftc1anclem8  38886  sdclem2  38942  ismtycnv  39002  heiborlem10  39020  lflvsass  40404  lkrscss  40421  eqlkr  40422  eqlkr3  40424  ldualvsdi2  40467  omllaw3  40568  cmtcomlemN  40571  cmtbr3N  40577  omlfh3N  40582  llnexchb2lem  41191  dalawlem7  41200  dalawlem11  41204  dalawlem12  41205  pol1N  41233  paddatclN  41272  4atexlemcnd  41395  ltrncoidN  41451  cdleme3b  41552  cdleme11  41593  cdleme15a  41597  cdleme22e  41667  cdleme22g  41671  cdlemg18b  42002  trlcoat  42046  cdlemk2  42155  cdlemk4  42157  cdlemki  42164  cdlemksv2  42170  cdlemk15  42178  cdlemk55a  42282  diainN  42380  dia2dimlem3  42389  dia2dimlem5  42391  dvhlveclem  42431  diaocN  42448  cdlemn4  42521  cdlemn8  42527  dihopelvalcpre  42571  dihmeetlem9N  42638  dih1dimatlem  42652  dihpN  42659  dochvalr3  42686  dochsat  42706  djhjlj  42726  dochdmm1  42733  dihjatcclem4  42744  dihjat1  42752  dihjat4  42756  dochsnkr2cl  42797  dochfl1  42799  lclkrlem2j  42839  mapdordlem2  42960  mapdrvallem2  42968  hdmap10  43163  lcmineqlem12  43356  3lexlogpow5ineq5  43376  aks4d1p1  43392  primrootsunit1  43413  primrootscoprmpow  43415  posbezout  43416  aks6d1c1p3  43426  aks6d1c1p4  43427  aks6d1c1p5  43428  aks6d1c1p7  43429  evl1gprodd  43433  hashscontpow1  43437  aks6d1c3  43439  aks6d1c2lem3  43442  aks6d1c2lem4  43443  aks6d1c2  43446  aks6d1c5lem3  43453  aks6d1c6lem1  43486  aks6d1c6isolem3  43492  aks6d1c6lem5  43493  bcle2d  43495  aks6d1c7lem1  43496  aks5lem3a  43505  grpods  43510  unitscyglem1  43511  unitscyglem2  43512  unitscyglem4  43514  unitscyglem5  43515  aks5lem7  43516  nicomachus  43635  sumcubes  43636  cnreeu  43820  frlmvscadiccat  43839  grpcominv1  43841  riccrng1  43848  ricdrng1  43858  frlmsnic  43870  evlselv  43883  fsuppind  43884  negexpidd  43958  3cubeslem2  43961  3cubeslem3r  43963  mzpsubmpt  44020  irrapxlem3  44097  pellexlem6  44107  pell1234qrne0  44126  pell1234qrreccl  44127  pell1234qrmulcl  44128  pell14qrdich  44142  pell1qrgaplem  44146  rmxluc  44209  rmyluc  44210  jm2.24nn  44232  jm2.18  44261  jm2.19lem2  44263  jm2.19lem3  44264  jm2.22  44268  jm2.23  44269  jm2.16nn0  44277  jm2.27c  44280  lmhmfgsplit  44354  hbtlem2  44391  onsucf1lem  44532  ofoafo  44619  naddcnffo  44627  naddwordnexlem4  44664  reabssgn  44897  relexpmulnn  44970  relexpmulg  44971  ntrclsneine0lem  45325  int-addassocd  45435  dvconstbi  45579  bccm1k  45587  binomcxplemnotnn0  45601  fmptsnxp  46457  wessf1ornlem  46473  projf1o  46484  infnsuprnmpt  46535  lefldiveq  46581  lt4addmuld  46595  fzdifsuc2  46599  suplesup  46624  infrpge  46636  xrlexaddrp  46637  xralrple2  46639  infleinflem1  46654  supminfrnmpt  46728  supminfxr2  46752  fsumnncl  46857  limcperiod  46913  sumnnodd  46915  limcresiooub  46925  limcresioolb  46926  0ellimcdiv  46932  reclimc  46936  limsupval3  46975  limsupequzmpt2  47001  liminfval5  47048  limsupresxr  47049  liminfresxr  47050  liminfvalxr  47066  liminfequzmpt2  47074  climliminflimsupd  47084  liminfltlem  47087  liminflbuz2  47098  sinmulcos  47148  coskpi2  47149  cncfdmsn  47173  cncfiooicclem1  47176  fprodsubrecnncnvlem  47190  fprodaddrecnncnvlem  47192  fperdvper  47202  dvnmptdivc  47221  dvnxpaek  47225  dvnmul  47226  dvnprodlem1  47229  dvnprodlem3  47231  itgcoscmulx  47252  itgsincmulx  47257  itgspltprt  47262  itgiccshift  47263  itgperiod  47264  sublevolico  47267  volioof  47270  ovolsplit  47271  fvvolioof  47272  fvvolicof  47274  stoweidlem22  47305  stoweidlem32  47315  wallispilem5  47352  stirlinglem5  47361  dirkertrigeqlem2  47382  dirkertrigeq  47384  dirkercncflem1  47386  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem13  47403  fourierdlem16  47406  fourierdlem19  47409  fourierdlem21  47411  fourierdlem22  47412  fourierdlem28  47418  fourierdlem32  47422  fourierdlem33  47423  fourierdlem42  47432  fourierdlem47  47436  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem56  47445  fourierdlem60  47449  fourierdlem61  47450  fourierdlem64  47453  fourierdlem66  47455  fourierdlem71  47460  fourierdlem73  47462  fourierdlem74  47463  fourierdlem76  47465  fourierdlem78  47467  fourierdlem79  47468  fourierdlem80  47469  fourierdlem81  47470  fourierdlem83  47472  fourierdlem88  47477  fourierdlem92  47481  fourierdlem93  47482  fourierdlem97  47486  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  fourierdlem109  47498  fourierdlem111  47500  fouriersw  47514  elaa2lem  47516  etransclem24  47541  etransclem25  47542  etransclem35  47552  etransclem46  47563  rrndistlt  47573  rrxunitopnfi  47575  qndenserrnbl  47578  qndenserrnopnlem  47580  saldifcl2  47611  intsal  47613  sge0sn  47662  sge0ltfirp  47683  sge0iunmptlemre  47698  sge0fodjrnlem  47699  sge0isum  47710  sge0xaddlem1  47716  nnfoctbdjlem  47738  meassle  47746  ismeannd  47750  meadif  47762  meaiuninclem  47763  meaiininclem  47769  omeunile  47788  caragendifcl  47797  caratheodory  47811  isomenndlem  47813  ovnsubaddlem1  47853  hoidmv1lelem2  47875  hoidmv1le  47877  hoidmvlelem2  47879  hoidmvle  47883  hoi2toco  47890  rrnmbl  47897  hoidifhspdmvle  47903  voncmpl  47904  hoiqssbl  47908  hspmbllem1  47909  hspmbllem2  47910  ovolval2lem  47926  ovolval5lem2  47936  ovnovollem1  47939  ovnovollem2  47940  hoimbl2  47948  vonhoire  47955  salpreimagelt  47990  salpreimalegt  47992  preimaioomnf  48002  smfres  48073  smfmullem1  48074  smflimmpt  48093  smfsupmpt  48098  smfinfmpt  48102  smflimsupmpt  48112  smfliminflem  48113  smfliminfmpt  48115  sigarcol  48147  sin5tlem2  48193  sinnpoly  48214  sqrtnpoly  48216  f1oresf1o  48633  elsprel  48830  prproropf1o  48862  paireqne  48866  sfprmdvdsmersenne  48961  lighneallem3  48965  lighneallem4  48968  nprmdvdsfacm1lem1  48978  nn0onn0exALTV  49070  nnsum3primesprm  49161  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  isuspgrim0lem  49264  clnbgrgrimlem  49304  uspgrlimlem3  49361  uspgrlimlem4  49362  gpgedgvtx0  49432  gpgedgvtx1  49433  funcringcsetcALTV2lem7  49666  funcringcsetclem7ALTV  49689  zellaz  49729  lincext3  49899  lincresunit3  49924  nn0onn0ex  49966  nnpw2pmod  50026  blennn0em1  50034  digexp  50050  dignn0ehalf  50060  nn0mulfsum  50067  itcovalpclem1  50113  eenglngeehlnmlem2  50182  rrx2vlinest  50184  line2  50195  itschlc0xyqsol  50210  itsclinecirc0b  50217  toplatjoin  50447  toplatmeet  50448  upeu2lem  50473  oppff1o  50596  imaf1co  50602  upciclem3  50615  natoppfb  50684  oppcthinco  50905  oppcthinendcALT  50907  lmddu  51181  tanhadd  51258  recsec  51277  reccsc  51278  aacllem  51367  crossp3d  51395  amgmlemALT  51416