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 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  3eqtrrd  2803  3eqtr2rd  2805  ifan  4541  ifor  4542  dfopif  4835  fnco  6653  fnsnfv  6960  nvocnv  7279  elovmpt3rab1  7670  onsucmin  7813  csbopeq1a  8043  oaabs2  8631  ecinxp  8786  resixpfo  8930  sbthlem3  9073  rankxpsuc  9850  fseqenlem2  10005  dfac2b  10110  isf32lem9  10340  compsscnvlem  10349  ttukeylem7  10494  fpwwe2lem10  10620  00id  11380  submul2  11649  mulsubfacd  11670  divadddiv  11925  infrenegsup  12193  xadd4d  13324  fzdifsuc  13608  fzval3  13759  fzoshftral  13812  ceim1l  13876  fldiv  13889  flmod  13914  intfrac  13915  modcyc2  13936  modaddb  13938  moddi  13971  uzrdgfni  13990  axdc4uzlem  14015  seqf1olem1  14073  seqf1olem2  14074  seqid2  14080  expnegz  14128  binom2sub  14252  binom3  14256  hashreshashfun  14472  ccatw2s1p2  14671  ccats1pfxeq  14747  pfxccatin12lem2  14764  pfxccatin12  14766  swrdccat3b  14773  cshweqrep  14854  2cshwcshw  14858  ccatco  14868  swrds2  14973  relexpsucnnr  15058  relexpaddnn  15084  sgnmul  15140  reim  15156  mulre  15168  addcj  15195  absimle  15356  clim2ser  15702  isercoll2  15716  serf0  15728  iseralt  15732  summolem3  15761  isumclim3  15806  mptfzshft  15825  fsumrev  15826  fsum2mul  15836  incexc  15887  isumsplit  15890  mertenslem1  15934  fprodrev  16027  iprodclim3  16050  binomfallfaclem2  16089  ef4p  16164  tanval3  16185  efival  16203  sinmul  16223  bitsinvp1  16502  sadaddlem  16519  bitsshft  16528  smu01lem  16538  dfgcd2  16599  lcmgcdlem  16659  lcm1  16663  lcmfass  16699  eulerthlem2  16836  hashgcdeq  16844  powm2modprm  16858  pythagtriplem16  16885  pczpre  16902  pcqdiv  16912  pcadd  16944  pcfac  16954  prmreclem5  16975  4sqlem10  17002  4sqlem19  17018  vdwapun  17029  vdwlem1  17036  ramcl  17084  setsstruct  17231  strfvd  17255  strfv2d  17256  xpsff1o  17616  xpsrnbas  17620  2oppccomf  17776  oppcepi  17791  sscfn1  17869  sscfn2  17870  invfuc  18029  funcestrcsetclem7  18197  funcsetcestrclem7  18212  gsumsplit1r  18740  grpinvssd  19078  grpinvval2  19084  cycsubggend  19271  pmtrdifwrdellem2  19547  psgnunilem1  19558  psgnuni  19564  pgp0  19661  sylow1lem1  19663  sylow3lem2  19693  efgredleme  19808  efgcpbllemb  19820  frgpuptinv  19836  frgpup3lem  19842  gexexlem  19917  cyggenod  19949  gsumval3eu  19969  gsumval3  19972  gsumzaddlem  19986  dprd2db  20110  ablsimpgfindlem1  20174  ringinvdv  20492  c0snmgmhm  20540  rngcifuestrc  20738  funcrngcsetc  20739  funcrngcsetcALT  20740  funcringcsetc  20773  lss1d  21084  pwssplit1  21180  rhmqusnsg  21425  rngqiprnglin  21442  znzrh2  21695  regsumsupp  21772  ipassr2  21797  dsmmfi  21888  frlmlss  21901  frlmip  21928  frlmlbs  21947  frlmup3  21950  islindf4  21988  mplcoe3  22189  subrgascl  22217  evlseu  22234  psdadd  22326  ply1sclid  22449  ply1chr  22466  evls1addd  22531  evls1muld  22532  evls1vsca  22533  evls1maprhm  22536  evls1maplmhm  22537  evls1maprnss  22538  evl1maprhm  22539  1marepvmarrepid  22732  madurid  22801  smadiadetlem3  22825  mat2pmatghm  22887  pmatcollpwscmatlem1  22946  pm2mpmhmlem2  22976  cpmadurid  23024  cpmidgsumm2pm  23026  cpmadugsumlemB  23031  cayhamlem2  23041  ntrval2  23208  ordtuni  23347  cnclima  23425  cmpsub  23557  ptbasfi  23738  txbasval  23763  pt1hmeo  23963  alexsubALTlem1  24204  trust  24386  ussid  24417  ressuss  24419  ressprdsds  24528  imasdsf1olem  24530  setsms  24637  tmsxms  24643  tmsxpsmopn  24694  subgnm  24790  tngnm  24808  tngngp2  24809  xrsxmet  24967  xrge0gsumle  24991  metdstri  25009  xrhmeo  25105  lebnumlem3  25122  pcorevlem  25185  pi1xfrcnvlem  25215  clmabs  25242  cvsmuleqdivd  25293  rrxip  25549  rrxds  25552  rrxdsfi  25570  minveclem4a  25589  pjthlem1  25596  divcncf  25606  ovolunlem1a  25655  mbfres2  25804  i1faddlem  25852  ibladdlem  25979  iblabs  25988  ditgsplit  26020  dvmptresicc  26075  dvnres  26090  dvmptdiv  26133  dveflem  26138  dveq0  26159  dvfsumabs  26182  itgsubstlem  26207  ply1divex  26294  r1pid2  26319  dgrco  26432  plycjlem  26433  taylthlem1  26536  pserdv2  26593  abelthlem6  26599  abelthlem7  26601  tangtx  26670  abssinper  26686  sineq0  26689  explog  26759  reexplog  26760  eflogeq  26767  abslogle  26783  tanarg  26784  logtayl  26825  logtayl2  26827  relogbdiv  26944  ang180lem3  26976  affineequiv  26988  affineequiv2  26989  chordthmlem4  27000  chordthmlem5  27001  heron  27003  dcubic1lem  27008  dcubic2  27009  dcubic  27011  mcubic  27012  cubic2  27013  dquartlem1  27016  dquart  27018  quart1lem  27020  quartlem1  27022  quart  27026  acoscos  27058  atanlogaddlem  27078  atantayl2  27103  atantayl3  27104  birthdaylem2  27117  efrlim  27134  amgmlem  27154  logdifbnd  27158  emcllem3  27162  emcllem6  27165  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem4  27196  lgamgulmlem5  27197  gamigam  27217  lgamcvg2  27219  gamfac  27231  basellem3  27247  basellem8  27252  basellem9  27253  chtprm  27317  logfaclbnd  27386  perfect1  27392  bcp1ctr  27443  bclbnd  27444  bposlem1  27448  lgsdilem  27488  lgsdirnn0  27508  lgsdinn0  27509  gausslemma2dlem1a  27529  gausslemma2dlem4  27533  gausslemma2dlem5a  27534  lgseisenlem2  27540  lgsquadlem1  27544  2sqlem2  27582  mul2sq  27583  2sqmod  27600  2sqnn0  27602  vmadivsum  27646  rpvmasumlem  27651  dchrisumlem1  27653  dchrisumlem2  27654  dchrmusum2  27658  dchrvmasum2if  27661  dchrisum0lem2  27682  logsqvma2  27707  selberg3  27723  selberg4lem1  27724  pntrsumo1  27729  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem5  27745  pntibndlem2  27755  pntlemk  27770  pntlemo  27771  ostth2lem4  27800  ostth3  27802  subsfo  28258  negsval2  28259  ltonold  28454  noseqrdgfn  28499  n0fincut  28548  addhalfcut  28652  bdayfinbndlem1  28660  z12shalf  28673  tgbtwndiff  28775  tgifscgr  28777  trgcgrg  28784  motcgr3  28814  tgbtwnconn1lem1  28841  tgbtwnconn1lem2  28842  ismir  28936  miriso  28947  midexlem  28969  symquadprlnglem  28970  ragmir  28980  footexALT  28998  footexlem1  28999  footexlem2  29000  colperpexlem3  29013  mideulem2  29015  midex  29018  opphllem3  29030  midcgr  29089  lmiisolem  29105  prlngmid2  29211  quadcgrprlng  29216  brbtwn2  29255  colinearalglem4  29259  axsegconlem1  29267  axpaschlem  29290  axcontlem4  29317  axcontlem7  29320  axcontlem8  29321  ushgredgedgloop  29581  crctcshwlkn0lem6  30164  wwlknlsw  30196  wwlksnextwrd  30246  clwlkclwwlklem2a3  30345  clwlkclwwlk2  30354  clwwlkel  30397  clwwlkfo  30401  clwwlkext2edg  30407  eupth2eucrct  30568  numclwwlk2lem1lem  30693  numclwwlk1lem2fo  30709  numclwlk2lem2f  30728  grpoidinvlem2  30857  nvmtri  31023  cnnvm  31034  nvnd  31040  ipidsq  31062  ipnm  31063  ipipcj  31067  blocnilem  31156  ipasslem2  31184  dipsubdir  31200  hvaddsubval  31385  pjhthlem1  31743  pjspansn  31929  pjo  32023  unoplin  32272  adjadj  32288  hmoplin  32294  eigvec1  32314  lnopeqi  32360  nmcexi  32378  lnfnsubi  32398  riesz3i  32414  kbass6  32473  leoprf2  32479  leoprf  32480  pjnmopi  32500  mdslmd1lem1  32677  mdslmd1lem2  32678  superpos  32706  ifeq3da  32892  fgreu  33016  cocnvf1o  33074  resf1o  33075  quad3d  33094  fprodex01  33169  ccatws1f1o  33271  wrdt2ind  33273  mndlactfo  33347  mndractfo  33349  gsummpt2d  33369  gsummptp1  33377  xrge0tsmseq  33395  gsumwrd2dccatlem  33397  gsumwrd2dccat  33398  symgfcoeu  33402  wrdpmtrlast  33413  psgnfzto1stlem  33420  psgnfzto1st  33425  cycpm2tr  33439  cycpmco2lem6  33451  cycpmco2lem7  33452  subrgchr  33556  elrgspnlem1  33562  elrgspnlem3  33564  elrgspnsubrunlem1  33567  rloccring  33591  rhmdvd  33644  qusrn  33718  nsgqusf1olem3  33724  rhmquskerlem  33733  elrspunsn  33737  mxidlirredi  33754  qsdrngi  33777  1arithidomlem1  33825  1arithidomlem2  33826  evls1subd  33862  deg1prod  33873  0mplrim  33904  evlextv  33932  psrmonprod  33942  esplyfval1  33963  esplyind  33965  esplyindfv  33966  esplyfvn  33967  vietalem  33969  resssra  33977  dimval  33991  dimvalfi  33992  lindsunlem  34014  dimkerim  34017  qusdimsum  34018  fedgmullem1  34019  extdg1id  34056  fldextrspunlsplem  34063  fldextrspunlsp  34064  fldextrspunlem1  34065  fldextrspundgdvds  34071  extdgfialglem1  34082  extdgfialglem2  34083  ply1annidllem  34091  algextdeglem4  34110  constrrtcc  34125  constrsslem  34131  constrresqrtcl  34167  cos9thpiminplylem2  34173  cos9thpiminply  34178  madjusmdetlem2  34218  qtophaus  34226  zarclssn  34263  zarcmplem  34271  pstmval  34285  mndpluscn  34316  qqhucn  34382  esumval  34436  gsumesum  34449  esumcst  34453  esumpcvgval  34468  oddpwdc  34744  eulerpartlemgvv  34766  probdif  34810  signsvtn  34971  actfunsnf1o  34991  reprpmtf1o  35013  hgt750lemd  35035  logdivsqrle  35037  hgt750lemg  35041  hgt750lemb  35043  bnj1415  35426  vonf1oonfo  35599  swrdrevpfx  35608  pfxwlk  35616  derangen2  35666  subfaclefac  35668  subfaclim  35680  satom  35848  fmla  35873  mrsubrn  36005  sinccvglem  36164  bcprod  36230  nmulss1  36691  filnetlem4  36892  curunc  38253  ltflcei  38259  matunitlindflem1  38267  matunitlindflem2  38268  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem24  38295  mblfinlem4  38311  ibladdnclem  38327  iblabsnc  38335  iblmulc2nc  38336  ftc1anclem6  38349  ftc1anclem8  38351  sdclem2  38393  ismtycnv  38453  heiborlem10  38471  lflvsass  39855  lkrscss  39872  eqlkr  39873  eqlkr3  39875  ldualvsdi2  39918  omllaw3  40019  cmtcomlemN  40022  cmtbr3N  40028  omlfh3N  40033  llnexchb2lem  40642  dalawlem7  40651  dalawlem11  40655  dalawlem12  40656  pol1N  40684  paddatclN  40723  4atexlemcnd  40846  ltrncoidN  40902  cdleme3b  41003  cdleme11  41044  cdleme15a  41048  cdleme22e  41118  cdleme22g  41122  cdlemg18b  41453  trlcoat  41497  cdlemk2  41606  cdlemk4  41608  cdlemki  41615  cdlemksv2  41621  cdlemk15  41629  cdlemk55a  41733  diainN  41831  dia2dimlem3  41840  dia2dimlem5  41842  dvhlveclem  41882  diaocN  41899  cdlemn4  41972  cdlemn8  41978  dihopelvalcpre  42022  dihmeetlem9N  42089  dih1dimatlem  42103  dihpN  42110  dochvalr3  42137  dochsat  42157  djhjlj  42177  dochdmm1  42184  dihjatcclem4  42195  dihjat1  42203  dihjat4  42207  dochsnkr2cl  42248  dochfl1  42250  lclkrlem2j  42290  mapdordlem2  42411  mapdrvallem2  42419  hdmap10  42614  lcmineqlem12  42807  3lexlogpow5ineq5  42827  aks4d1p1  42843  primrootsunit1  42864  primrootscoprmpow  42866  posbezout  42867  aks6d1c1p3  42877  aks6d1c1p4  42878  aks6d1c1p5  42879  aks6d1c1p7  42880  evl1gprodd  42884  hashscontpow1  42888  aks6d1c3  42890  aks6d1c2lem3  42893  aks6d1c2lem4  42894  aks6d1c2  42897  aks6d1c5lem3  42904  aks6d1c6lem1  42937  aks6d1c6isolem3  42943  aks6d1c6lem5  42944  bcle2d  42946  aks6d1c7lem1  42947  aks5lem3a  42956  grpods  42961  unitscyglem1  42962  unitscyglem2  42963  unitscyglem4  42965  unitscyglem5  42966  aks5lem7  42967  nicomachus  43073  sumcubes  43074  cnreeu  43264  frlmvscadiccat  43280  grpcominv1  43282  riccrng1  43289  ricdrng1  43296  frlmsnic  43308  evlselv  43321  fsuppind  43322  flt4lem7  43391  negexpidd  43413  3cubeslem2  43416  3cubeslem3r  43418  mzpsubmpt  43474  irrapxlem3  43551  pellexlem6  43561  pell1234qrne0  43580  pell1234qrreccl  43581  pell1234qrmulcl  43582  pell14qrdich  43596  pell1qrgaplem  43600  rmxluc  43663  rmyluc  43664  jm2.24nn  43686  jm2.18  43715  jm2.19lem2  43717  jm2.19lem3  43718  jm2.22  43722  jm2.23  43723  jm2.16nn0  43731  jm2.27c  43734  fnwe2lem2  43778  lmhmfgsplit  43813  hbtlem2  43851  onsucf1lem  43996  ofoafo  44083  naddcnffo  44091  naddwordnexlem4  44128  reabssgn  44362  relexpmulnn  44435  relexpmulg  44436  ntrclsneine0lem  44790  int-addassocd  44900  dvconstbi  45044  bccm1k  45052  binomcxplemnotnn0  45066  fmptsnxp  45887  wessf1ornlem  45903  projf1o  45914  infnsuprnmpt  45965  lefldiveq  46011  lt4addmuld  46025  fzdifsuc2  46029  suplesup  46055  infrpge  46067  xrlexaddrp  46068  xralrple2  46070  infleinflem1  46085  supminfrnmpt  46159  supminfxr2  46183  fsumnncl  46288  limcperiod  46344  sumnnodd  46346  limcresiooub  46356  limcresioolb  46357  0ellimcdiv  46363  reclimc  46367  limsupval3  46406  limsupequzmpt2  46432  liminfval5  46479  limsupresxr  46480  liminfresxr  46481  liminfvalxr  46497  liminfequzmpt2  46505  climliminflimsupd  46515  liminfltlem  46518  liminflbuz2  46529  sinmulcos  46579  coskpi2  46580  cncfdmsn  46604  cncfiooicclem1  46607  fprodsubrecnncnvlem  46621  fprodaddrecnncnvlem  46623  fperdvper  46633  dvnmptdivc  46652  dvnxpaek  46656  dvnmul  46657  dvnprodlem1  46660  dvnprodlem3  46662  itgcoscmulx  46683  itgsincmulx  46688  itgspltprt  46693  itgiccshift  46694  itgperiod  46695  sublevolico  46698  volioof  46701  ovolsplit  46702  fvvolioof  46703  fvvolicof  46705  stoweidlem22  46736  stoweidlem32  46746  wallispilem5  46783  stirlinglem5  46792  dirkertrigeqlem2  46813  dirkertrigeq  46815  dirkercncflem1  46817  dirkercncflem2  46818  dirkercncflem4  46820  fourierdlem13  46834  fourierdlem16  46837  fourierdlem19  46840  fourierdlem21  46842  fourierdlem22  46843  fourierdlem28  46849  fourierdlem32  46853  fourierdlem33  46854  fourierdlem42  46863  fourierdlem47  46867  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem56  46876  fourierdlem60  46880  fourierdlem61  46881  fourierdlem64  46884  fourierdlem66  46886  fourierdlem71  46891  fourierdlem73  46893  fourierdlem74  46894  fourierdlem76  46896  fourierdlem78  46898  fourierdlem79  46899  fourierdlem80  46900  fourierdlem81  46901  fourierdlem83  46903  fourierdlem88  46908  fourierdlem92  46912  fourierdlem93  46913  fourierdlem97  46917  fourierdlem101  46921  fourierdlem103  46923  fourierdlem104  46924  fourierdlem109  46929  fourierdlem111  46931  fouriersw  46945  elaa2lem  46947  etransclem24  46972  etransclem25  46973  etransclem35  46983  etransclem46  46994  rrndistlt  47004  rrxunitopnfi  47006  qndenserrnbl  47009  qndenserrnopnlem  47011  saldifcl2  47042  intsal  47044  sge0sn  47093  sge0ltfirp  47114  sge0iunmptlemre  47129  sge0fodjrnlem  47130  sge0isum  47141  sge0xaddlem1  47147  nnfoctbdjlem  47169  meassle  47177  ismeannd  47181  meadif  47193  meaiuninclem  47194  meaiininclem  47200  omeunile  47219  caragendifcl  47228  caratheodory  47242  isomenndlem  47244  ovnsubaddlem1  47284  hoidmv1lelem2  47306  hoidmv1le  47308  hoidmvlelem2  47310  hoidmvle  47314  hoi2toco  47321  rrnmbl  47328  hoidifhspdmvle  47334  voncmpl  47335  hoiqssbl  47339  hspmbllem1  47340  hspmbllem2  47341  ovolval2lem  47357  ovolval5lem2  47367  ovnovollem1  47370  ovnovollem2  47371  hoimbl2  47379  vonhoire  47386  salpreimagelt  47421  salpreimalegt  47423  preimaioomnf  47433  smfres  47504  smfmullem1  47505  smflimmpt  47524  smfsupmpt  47529  smfinfmpt  47533  smflimsupmpt  47543  smfliminflem  47544  smfliminfmpt  47546  sigarcol  47578  sin5tlem2  47611  f1oresf1o  48027  elsprel  48224  prproropf1o  48256  paireqne  48260  sfprmdvdsmersenne  48355  lighneallem3  48359  lighneallem4  48362  nprmdvdsfacm1lem1  48372  nn0onn0exALTV  48464  nnsum3primesprm  48555  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  isuspgrim0lem  48658  clnbgrgrimlem  48698  uspgrlimlem3  48755  uspgrlimlem4  48756  gpgedgvtx0  48826  gpgedgvtx1  48827  funcringcsetcALTV2lem7  49061  funcringcsetclem7ALTV  49084  lincext3  49236  lincresunit3  49261  nn0onn0ex  49303  nnpw2pmod  49363  blennn0em1  49371  digexp  49387  dignn0ehalf  49397  nn0mulfsum  49404  itcovalpclem1  49450  eenglngeehlnmlem2  49518  rrx2vlinest  49521  line2  49532  itschlc0xyqsol  49547  itsclinecirc0b  49554  toplatjoin  49780  toplatmeet  49781  upeu2lem  49806  oppff1o  49927  imaf1co  49933  upciclem3  49946  natoppfb  50009  oppcthinco  50217  oppcthinendcALT  50219  lmddu  50445  recsec  50534  reccsc  50535  aacllem  50621  amgmlemALT  50623