Theorem eqtr2d 2769

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  3eqtrrd  2773  3eqtr2rd  2775  ifan  4530  ifor  4531  dfopif  4823  fnco  6607  fnsnfv  6910  nvocnv  7224  elovmpt3rab1  7615  onsucmin  7760  csbopeq1a  7991  oaabs2  8573  ecinxp  8725  resixpfo  8870  sbthlem3  9013  rankxpsuc  9786  fseqenlem2  9927  dfac2b  10033  isf32lem9  10263  compsscnvlem  10272  ttukeylem7  10417  fpwwe2lem10  10542  00id  11299  submul2  11568  mulsubfacd  11589  divadddiv  11847  infrenegsup  12116  xadd4d  13209  fzdifsuc  13491  fzval3  13641  fzoshftral  13694  ceim1l  13758  fldiv  13771  flmod  13796  intfrac  13797  modcyc2  13818  modaddb  13820  moddi  13853  uzrdgfni  13872  axdc4uzlem  13897  seqf1olem1  13955  seqf1olem2  13956  seqid2  13962  expnegz  14010  binom2sub  14134  binom3  14138  hashreshashfun  14353  ccatw2s1p2  14552  ccats1pfxeq  14628  pfxccatin12lem2  14645  pfxccatin12  14647  swrdccat3b  14654  cshweqrep  14735  2cshwcshw  14739  ccatco  14749  swrds2  14854  relexpsucnnr  14939  relexpaddnn  14965  reim  15023  mulre  15035  addcj  15062  absimle  15223  clim2ser  15569  isercoll2  15583  serf0  15595  iseralt  15599  summolem3  15628  isumclim3  15673  mptfzshft  15692  fsumrev  15693  fsum2mul  15703  incexc  15751  isumsplit  15754  mertenslem1  15798  fprodrev  15891  iprodclim3  15914  binomfallfaclem2  15954  ef4p  16029  tanval3  16050  efival  16068  sinmul  16088  bitsinvp1  16367  sadaddlem  16384  bitsshft  16393  smu01lem  16403  dfgcd2  16464  lcmgcdlem  16524  lcm1  16528  lcmfass  16564  eulerthlem2  16700  hashgcdeq  16708  powm2modprm  16722  pythagtriplem16  16749  pczpre  16766  pcqdiv  16776  pcadd  16808  pcfac  16818  prmreclem5  16839  4sqlem10  16866  4sqlem19  16882  vdwapun  16893  vdwlem1  16900  ramcl  16948  setsstruct  17094  strfvd  17118  strfv2d  17119  xpsff1o  17479  xpsrnbas  17483  2oppccomf  17639  oppcepi  17654  sscfn1  17732  sscfn2  17733  invfuc  17892  funcestrcsetclem7  18060  funcsetcestrclem7  18075  gsumsplit1r  18603  grpinvssd  18938  grpinvval2  18944  cycsubggend  19125  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  20341  c0snmgmhm  20389  rngcifuestrc  20563  funcrngcsetc  20564  funcrngcsetcALT  20565  funcringcsetc  20598  lss1d  20905  pwssplit1  21002  rhmqusnsg  21231  rngqiprnglin  21248  znzrh2  21491  regsumsupp  21568  ipassr2  21593  dsmmfi  21684  frlmlss  21697  frlmip  21724  frlmlbs  21743  frlmup3  21746  islindf4  21784  mplcoe3  21984  subrgascl  22012  evlseu  22029  psdadd  22097  ply1sclid  22221  ply1chr  22241  evls1addd  22306  evls1muld  22307  evls1vsca  22308  evls1maprhm  22311  evls1maplmhm  22312  evls1maprnss  22313  evl1maprhm  22314  1marepvmarrepid  22510  madurid  22579  smadiadetlem3  22603  mat2pmatghm  22665  pmatcollpwscmatlem1  22724  pm2mpmhmlem2  22754  cpmadurid  22802  cpmidgsumm2pm  22804  cpmadugsumlemB  22809  cayhamlem2  22819  ntrval2  22986  ordtuni  23125  cnclima  23203  cmpsub  23335  ptbasfi  23516  txbasval  23541  pt1hmeo  23741  alexsubALTlem1  23982  trust  24164  ussid  24195  ressuss  24197  ressprdsds  24306  imasdsf1olem  24308  setsms  24415  tmsxms  24421  tmsxpsmopn  24472  subgnm  24568  tngnm  24586  tngngp2  24587  xrsxmet  24745  xrge0gsumle  24769  metdstri  24787  xrhmeo  24891  lebnumlem3  24909  pcorevlem  24973  pi1xfrcnvlem  25003  clmabs  25030  cvsmuleqdivd  25081  rrxip  25337  rrxds  25340  rrxdsfi  25358  minveclem4a  25377  pjthlem1  25384  divcncf  25395  ovolunlem1a  25444  mbfres2  25593  i1faddlem  25641  ibladdlem  25768  iblabs  25777  ditgsplit  25809  dvmptresicc  25864  dvnres  25880  dvmptdiv  25925  dveflem  25930  dveq0  25952  dvfsumabs  25976  itgsubstlem  26002  ply1divex  26089  r1pid2  26114  dgrco  26228  plycjlem  26229  taylthlem1  26328  pserdv2  26387  abelthlem6  26393  abelthlem7  26395  tangtx  26461  abssinper  26477  sineq0  26480  explog  26550  reexplog  26551  eflogeq  26558  abslogle  26574  tanarg  26575  logtayl  26616  logtayl2  26618  relogbdiv  26736  ang180lem3  26768  affineequiv  26780  affineequiv2  26781  chordthmlem4  26792  chordthmlem5  26793  heron  26795  dcubic1lem  26800  dcubic2  26801  dcubic  26803  mcubic  26804  cubic2  26805  dquartlem1  26808  dquart  26810  quart1lem  26812  quartlem1  26814  quart  26818  acoscos  26850  atanlogaddlem  26870  atantayl2  26895  atantayl3  26896  birthdaylem2  26909  efrlim  26926  efrlimOLD  26927  amgmlem  26947  logdifbnd  26951  emcllem3  26955  emcllem6  26958  lgamgulmlem2  26987  lgamgulmlem3  26988  lgamgulmlem4  26989  lgamgulmlem5  26990  gamigam  27010  lgamcvg2  27012  gamfac  27024  basellem3  27040  basellem8  27045  basellem9  27046  chtprm  27110  logfaclbnd  27180  perfect1  27186  bcp1ctr  27237  bclbnd  27238  bposlem1  27242  lgsdilem  27282  lgsdirnn0  27302  lgsdinn0  27303  gausslemma2dlem1a  27323  gausslemma2dlem4  27327  gausslemma2dlem5a  27328  lgseisenlem2  27334  lgsquadlem1  27338  2sqlem2  27376  mul2sq  27377  2sqmod  27394  2sqnn0  27396  vmadivsum  27440  rpvmasumlem  27445  dchrisumlem1  27447  dchrisumlem2  27448  dchrmusum2  27452  dchrvmasum2if  27455  dchrisum0lem2  27476  logsqvma2  27501  selberg3  27517  selberg4lem1  27518  pntrsumo1  27523  pntrlog2bndlem2  27536  pntrlog2bndlem3  27537  pntrlog2bndlem5  27539  pntibndlem2  27549  pntlemk  27564  pntlemo  27565  ostth2lem4  27594  ostth3  27596  subsfo  28025  negsval2  28026  sltonold  28218  noseqrdgfn  28256  n0sfincut  28302  addhalfcut  28399  zs12half  28410  tgbtwndiff  28504  tgifscgr  28506  trgcgrg  28513  motcgr3  28543  tgbtwnconn1lem1  28570  tgbtwnconn1lem2  28571  ismir  28657  miriso  28668  midexlem  28690  ragmir  28698  footexALT  28716  footexlem1  28717  footexlem2  28718  colperpexlem3  28730  mideulem2  28732  midex  28735  opphllem3  28747  midcgr  28778  lmiisolem  28794  brbtwn2  28904  colinearalglem4  28908  axsegconlem1  28916  axpaschlem  28939  axcontlem4  28966  axcontlem7  28969  axcontlem8  28970  ushgredgedgloop  29230  crctcshwlkn0lem6  29814  wwlknlsw  29846  wwlksnextwrd  29896  clwlkclwwlklem2a3  29995  clwlkclwwlk2  30004  clwwlkel  30047  clwwlkfo  30051  clwwlkext2edg  30057  eupth2eucrct  30218  numclwwlk2lem1lem  30343  numclwwlk1lem2fo  30359  numclwlk2lem2f  30378  grpoidinvlem2  30506  nvmtri  30672  cnnvm  30683  nvnd  30689  ipidsq  30711  ipnm  30712  ipipcj  30716  blocnilem  30805  ipasslem2  30833  dipsubdir  30849  hvaddsubval  31034  pjhthlem1  31392  pjspansn  31578  pjo  31672  unoplin  31921  adjadj  31937  hmoplin  31943  eigvec1  31963  lnopeqi  32009  nmcexi  32027  lnfnsubi  32047  riesz3i  32063  kbass6  32122  leoprf2  32128  leoprf  32129  pjnmopi  32149  mdslmd1lem1  32326  mdslmd1lem2  32327  superpos  32355  ifeq3da  32547  fresunsn  32629  fgreu  32676  cocnvf1o  32736  resf1o  32737  quad3d  32757  fprodex01  32834  sgnmul  32844  ccatws1f1o  32961  wrdt2ind  32963  mndlactfo  33037  mndractfo  33039  gsummpt2d  33060  gsummptp1  33068  xrge0tsmseq  33085  gsumwrd2dccatlem  33087  gsumwrd2dccat  33088  symgfcoeu  33092  wrdpmtrlast  33103  psgnfzto1stlem  33110  psgnfzto1st  33115  cycpm2tr  33129  cycpmco2lem6  33141  cycpmco2lem7  33142  subrgchr  33247  elrgspnlem1  33252  elrgspnlem3  33254  elrgspnsubrunlem1  33257  rloccring  33280  rhmdvd  33333  qusrn  33418  nsgqusf1olem3  33424  rhmquskerlem  33434  elrspunsn  33438  mxidlirredi  33480  qsdrngi  33504  1arithidomlem1  33544  1arithidomlem2  33545  evls1subd  33581  deg1prod  33592  r1pid2OLD  33618  evlextv  33635  esplyind  33659  esplyindfv  33660  esplyfvn  33661  vietalem  33663  resssra  33671  dimval  33685  dimvalfi  33686  lindsunlem  33709  dimkerim  33712  qusdimsum  33713  fedgmullem1  33714  extdg1id  33751  fldextrspunlsplem  33758  fldextrspunlsp  33759  fldextrspunlem1  33760  fldextrspundgdvds  33766  extdgfialglem1  33777  extdgfialglem2  33778  ply1annidllem  33786  algextdeglem4  33805  constrrtcc  33820  constrsslem  33826  constrresqrtcl  33862  cos9thpiminplylem2  33868  cos9thpiminply  33873  madjusmdetlem2  33913  qtophaus  33921  zarclssn  33958  zarcmplem  33966  pstmval  33980  mndpluscn  34011  qqhucn  34077  esumval  34131  gsumesum  34144  esumcst  34148  esumpcvgval  34163  oddpwdc  34439  eulerpartlemgvv  34461  probdif  34505  signsvtn  34669  actfunsnf1o  34689  reprpmtf1o  34711  hgt750lemd  34733  logdivsqrle  34735  hgt750lemg  34739  hgt750lemb  34741  bnj1415  35122  swrdrevpfx  35233  pfxwlk  35240  derangen2  35290  subfaclefac  35292  subfaclim  35304  satom  35472  fmla  35497  mrsubrn  35629  sinccvglem  35788  bcprod  35854  filnetlem4  36497  curunc  37715  ltflcei  37721  matunitlindflem1  37729  matunitlindflem2  37730  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem24  37757  mblfinlem4  37773  ibladdnclem  37789  iblabsnc  37797  iblmulc2nc  37798  ftc1anclem6  37811  ftc1anclem8  37813  sdclem2  37855  ismtycnv  37915  heiborlem10  37933  lflvsass  39253  lkrscss  39270  eqlkr  39271  eqlkr3  39273  ldualvsdi2  39316  omllaw3  39417  cmtcomlemN  39420  cmtbr3N  39426  omlfh3N  39431  llnexchb2lem  40040  dalawlem7  40049  dalawlem11  40053  dalawlem12  40054  pol1N  40082  paddatclN  40121  4atexlemcnd  40244  ltrncoidN  40300  cdleme3b  40401  cdleme11  40442  cdleme15a  40446  cdleme22e  40516  cdleme22g  40520  cdlemg18b  40851  trlcoat  40895  cdlemk2  41004  cdlemk4  41006  cdlemki  41013  cdlemksv2  41019  cdlemk15  41027  cdlemk55a  41131  diainN  41229  dia2dimlem3  41238  dia2dimlem5  41240  dvhlveclem  41280  diaocN  41297  cdlemn4  41370  cdlemn8  41376  dihopelvalcpre  41420  dihmeetlem9N  41487  dih1dimatlem  41501  dihpN  41508  dochvalr3  41535  dochsat  41555  djhjlj  41575  dochdmm1  41582  dihjatcclem4  41593  dihjat1  41601  dihjat4  41605  dochsnkr2cl  41646  dochfl1  41648  lclkrlem2j  41688  mapdordlem2  41809  mapdrvallem2  41817  hdmap10  42012  lcmineqlem12  42206  3lexlogpow5ineq5  42226  aks4d1p1  42242  primrootsunit1  42263  primrootscoprmpow  42265  posbezout  42266  aks6d1c1p3  42276  aks6d1c1p4  42277  aks6d1c1p5  42278  aks6d1c1p7  42279  evl1gprodd  42283  hashscontpow1  42287  aks6d1c3  42289  aks6d1c2lem3  42292  aks6d1c2lem4  42293  aks6d1c2  42296  aks6d1c5lem3  42303  aks6d1c6lem1  42336  aks6d1c6isolem3  42342  aks6d1c6lem5  42343  bcle2d  42345  aks6d1c7lem1  42346  aks5lem3a  42355  grpods  42360  unitscyglem1  42361  unitscyglem2  42362  unitscyglem4  42364  unitscyglem5  42365  aks5lem7  42366  nicomachus  42482  sumcubes  42483  cnreeu  42660  frlmvscadiccat  42676  grpcominv1  42678  riccrng1  42691  ricdrng1  42698  frlmsnic  42710  evlselv  42745  fsuppind  42748  flt4lem7  42817  negexpidd  42839  3cubeslem2  42842  3cubeslem3r  42844  mzpsubmpt  42900  irrapxlem3  42981  pellexlem6  42991  pell1234qrne0  43010  pell1234qrreccl  43011  pell1234qrmulcl  43012  pell14qrdich  43026  pell1qrgaplem  43030  rmxluc  43093  rmyluc  43094  jm2.24nn  43116  jm2.18  43145  jm2.19lem2  43147  jm2.19lem3  43148  jm2.22  43152  jm2.23  43153  jm2.16nn0  43161  jm2.27c  43164  fnwe2lem2  43208  lmhmfgsplit  43243  hbtlem2  43281  onsucf1lem  43426  ofoafo  43513  naddcnffo  43521  naddwordnexlem4  43558  reabssgn  43793  relexpmulnn  43866  relexpmulg  43867  ntrclsneine0lem  44221  int-addassocd  44331  dvconstbi  44491  bccm1k  44499  binomcxplemnotnn0  44513  fmptsnxp  45329  wessf1ornlem  45345  projf1o  45357  infnsuprnmpt  45410  lefldiveq  45456  lt4addmuld  45470  fzdifsuc2  45474  suplesup  45500  infrpge  45512  xrlexaddrp  45513  xralrple2  45515  infleinflem1  45530  supminfrnmpt  45605  supminfxr2  45629  fsumnncl  45734  limcperiod  45790  sumnnodd  45792  limcresiooub  45802  limcresioolb  45803  0ellimcdiv  45809  reclimc  45813  limsupval3  45852  limsupequzmpt2  45878  liminfval5  45925  limsupresxr  45926  liminfresxr  45927  liminfvalxr  45943  liminfequzmpt2  45951  climliminflimsupd  45961  liminfltlem  45964  liminflbuz2  45975  sinmulcos  46025  coskpi2  46026  cncfdmsn  46050  cncfiooicclem1  46053  fprodsubrecnncnvlem  46067  fprodaddrecnncnvlem  46069  fperdvper  46079  dvnmptdivc  46098  dvnxpaek  46102  dvnmul  46103  dvnprodlem1  46106  dvnprodlem3  46108  itgcoscmulx  46129  itgsincmulx  46134  itgspltprt  46139  itgiccshift  46140  itgperiod  46141  sublevolico  46144  volioof  46147  ovolsplit  46148  fvvolioof  46149  fvvolicof  46151  stoweidlem22  46182  stoweidlem32  46192  wallispilem5  46229  stirlinglem5  46238  dirkertrigeqlem2  46259  dirkertrigeq  46261  dirkercncflem1  46263  dirkercncflem2  46264  dirkercncflem4  46266  fourierdlem13  46280  fourierdlem16  46283  fourierdlem19  46286  fourierdlem21  46288  fourierdlem22  46289  fourierdlem28  46295  fourierdlem32  46299  fourierdlem33  46300  fourierdlem42  46309  fourierdlem47  46313  fourierdlem48  46314  fourierdlem49  46315  fourierdlem50  46316  fourierdlem56  46322  fourierdlem60  46326  fourierdlem61  46327  fourierdlem64  46330  fourierdlem66  46332  fourierdlem71  46337  fourierdlem73  46339  fourierdlem74  46340  fourierdlem76  46342  fourierdlem78  46344  fourierdlem79  46345  fourierdlem80  46346  fourierdlem81  46347  fourierdlem83  46349  fourierdlem88  46354  fourierdlem92  46358  fourierdlem93  46359  fourierdlem97  46363  fourierdlem101  46367  fourierdlem103  46369  fourierdlem104  46370  fourierdlem109  46375  fourierdlem111  46377  fouriersw  46391  elaa2lem  46393  etransclem24  46418  etransclem25  46419  etransclem35  46429  etransclem46  46440  rrndistlt  46450  rrxunitopnfi  46452  qndenserrnbl  46455  qndenserrnopnlem  46457  saldifcl2  46488  intsal  46490  sge0sn  46539  sge0ltfirp  46560  sge0iunmptlemre  46575  sge0fodjrnlem  46576  sge0isum  46587  sge0xaddlem1  46593  nnfoctbdjlem  46615  meassle  46623  ismeannd  46627  meadif  46639  meaiuninclem  46640  meaiininclem  46646  omeunile  46665  caragendifcl  46674  caratheodory  46688  isomenndlem  46690  ovnsubaddlem1  46730  hoidmv1lelem2  46752  hoidmv1le  46754  hoidmvlelem2  46756  hoidmvle  46760  hoi2toco  46767  rrnmbl  46774  hoidifhspdmvle  46780  voncmpl  46781  hoiqssbl  46785  hspmbllem1  46786  hspmbllem2  46787  ovolval2lem  46803  ovolval5lem2  46813  ovnovollem1  46816  ovnovollem2  46817  hoimbl2  46825  vonhoire  46832  salpreimagelt  46867  salpreimalegt  46869  preimaioomnf  46879  smfres  46950  smfmullem1  46951  smflimmpt  46970  smfsupmpt  46975  smfinfmpt  46979  smflimsupmpt  46989  smfliminflem  46990  smfliminfmpt  46992  sigarcol  47024  f1oresf1o  47452  elsprel  47637  prproropf1o  47669  paireqne  47673  sfprmdvdsmersenne  47765  lighneallem3  47769  lighneallem4  47772  nn0onn0exALTV  47861  nnsum3primesprm  47952  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  isuspgrim0lem  48055  clnbgrgrimlem  48095  uspgrlimlem3  48152  uspgrlimlem4  48153  gpgedgvtx0  48223  gpgedgvtx1  48224  funcringcsetcALTV2lem7  48458  funcringcsetclem7ALTV  48481  lincext3  48618  lincresunit3  48643  nn0onn0ex  48685  nnpw2pmod  48745  blennn0em1  48753  digexp  48769  dignn0ehalf  48779  nn0mulfsum  48786  itcovalpclem1  48832  eenglngeehlnmlem2  48900  rrx2vlinest  48903  line2  48914  itschlc0xyqsol  48929  itsclinecirc0b  48936  toplatjoin  49163  toplatmeet  49164  upeu2lem  49189  oppff1o  49310  imaf1co  49316  upciclem3  49329  natoppfb  49392  oppcthinco  49600  oppcthinendcALT  49602  lmddu  49828  recsec  49917  reccsc  49918  aacllem  49962  amgmlemALT  49964