Theorem eqtr2d 2772

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 2771	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2742	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 2708

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

This theorem is referenced by:  3eqtrrd  2776  3eqtr2rd  2778  ifan  4533  ifor  4534  dfopif  4826  fnco  6610  fnsnfv  6913  nvocnv  7227  elovmpt3rab1  7618  onsucmin  7763  csbopeq1a  7994  oaabs2  8577  ecinxp  8729  resixpfo  8874  sbthlem3  9017  rankxpsuc  9794  fseqenlem2  9935  dfac2b  10041  isf32lem9  10271  compsscnvlem  10280  ttukeylem7  10425  fpwwe2lem10  10551  00id  11308  submul2  11577  mulsubfacd  11598  divadddiv  11856  infrenegsup  12125  xadd4d  13218  fzdifsuc  13500  fzval3  13650  fzoshftral  13703  ceim1l  13767  fldiv  13780  flmod  13805  intfrac  13806  modcyc2  13827  modaddb  13829  moddi  13862  uzrdgfni  13881  axdc4uzlem  13906  seqf1olem1  13964  seqf1olem2  13965  seqid2  13971  expnegz  14019  binom2sub  14143  binom3  14147  hashreshashfun  14362  ccatw2s1p2  14561  ccats1pfxeq  14637  pfxccatin12lem2  14654  pfxccatin12  14656  swrdccat3b  14663  cshweqrep  14744  2cshwcshw  14748  ccatco  14758  swrds2  14863  relexpsucnnr  14948  relexpaddnn  14974  reim  15032  mulre  15044  addcj  15071  absimle  15232  clim2ser  15578  isercoll2  15592  serf0  15604  iseralt  15608  summolem3  15637  isumclim3  15682  mptfzshft  15701  fsumrev  15702  fsum2mul  15712  incexc  15760  isumsplit  15763  mertenslem1  15807  fprodrev  15900  iprodclim3  15923  binomfallfaclem2  15963  ef4p  16038  tanval3  16059  efival  16077  sinmul  16097  bitsinvp1  16376  sadaddlem  16393  bitsshft  16402  smu01lem  16412  dfgcd2  16473  lcmgcdlem  16533  lcm1  16537  lcmfass  16573  eulerthlem2  16709  hashgcdeq  16717  powm2modprm  16731  pythagtriplem16  16758  pczpre  16775  pcqdiv  16785  pcadd  16817  pcfac  16827  prmreclem5  16848  4sqlem10  16875  4sqlem19  16891  vdwapun  16902  vdwlem1  16909  ramcl  16957  setsstruct  17103  strfvd  17127  strfv2d  17128  xpsff1o  17488  xpsrnbas  17492  2oppccomf  17648  oppcepi  17663  sscfn1  17741  sscfn2  17742  invfuc  17901  funcestrcsetclem7  18069  funcsetcestrclem7  18084  gsumsplit1r  18612  grpinvssd  18947  grpinvval2  18953  cycsubggend  19134  pmtrdifwrdellem2  19411  psgnunilem1  19422  psgnuni  19428  pgp0  19525  sylow1lem1  19527  sylow3lem2  19557  efgredleme  19672  efgcpbllemb  19684  frgpuptinv  19700  frgpup3lem  19706  gexexlem  19781  cyggenod  19813  gsumval3eu  19833  gsumval3  19836  gsumzaddlem  19850  dprd2db  19974  ablsimpgfindlem1  20038  ringinvdv  20350  c0snmgmhm  20398  rngcifuestrc  20572  funcrngcsetc  20573  funcrngcsetcALT  20574  funcringcsetc  20607  lss1d  20914  pwssplit1  21011  rhmqusnsg  21240  rngqiprnglin  21257  znzrh2  21500  regsumsupp  21577  ipassr2  21602  dsmmfi  21693  frlmlss  21706  frlmip  21733  frlmlbs  21752  frlmup3  21755  islindf4  21793  mplcoe3  21993  subrgascl  22021  evlseu  22038  psdadd  22106  ply1sclid  22230  ply1chr  22250  evls1addd  22315  evls1muld  22316  evls1vsca  22317  evls1maprhm  22320  evls1maplmhm  22321  evls1maprnss  22322  evl1maprhm  22323  1marepvmarrepid  22519  madurid  22588  smadiadetlem3  22612  mat2pmatghm  22674  pmatcollpwscmatlem1  22733  pm2mpmhmlem2  22763  cpmadurid  22811  cpmidgsumm2pm  22813  cpmadugsumlemB  22818  cayhamlem2  22828  ntrval2  22995  ordtuni  23134  cnclima  23212  cmpsub  23344  ptbasfi  23525  txbasval  23550  pt1hmeo  23750  alexsubALTlem1  23991  trust  24173  ussid  24204  ressuss  24206  ressprdsds  24315  imasdsf1olem  24317  setsms  24424  tmsxms  24430  tmsxpsmopn  24481  subgnm  24577  tngnm  24595  tngngp2  24596  xrsxmet  24754  xrge0gsumle  24778  metdstri  24796  xrhmeo  24900  lebnumlem3  24918  pcorevlem  24982  pi1xfrcnvlem  25012  clmabs  25039  cvsmuleqdivd  25090  rrxip  25346  rrxds  25349  rrxdsfi  25367  minveclem4a  25386  pjthlem1  25393  divcncf  25404  ovolunlem1a  25453  mbfres2  25602  i1faddlem  25650  ibladdlem  25777  iblabs  25786  ditgsplit  25818  dvmptresicc  25873  dvnres  25889  dvmptdiv  25934  dveflem  25939  dveq0  25961  dvfsumabs  25985  itgsubstlem  26011  ply1divex  26098  r1pid2  26123  dgrco  26237  plycjlem  26238  taylthlem1  26337  pserdv2  26396  abelthlem6  26402  abelthlem7  26404  tangtx  26470  abssinper  26486  sineq0  26489  explog  26559  reexplog  26560  eflogeq  26567  abslogle  26583  tanarg  26584  logtayl  26625  logtayl2  26627  relogbdiv  26745  ang180lem3  26777  affineequiv  26789  affineequiv2  26790  chordthmlem4  26801  chordthmlem5  26802  heron  26804  dcubic1lem  26809  dcubic2  26810  dcubic  26812  mcubic  26813  cubic2  26814  dquartlem1  26817  dquart  26819  quart1lem  26821  quartlem1  26823  quart  26827  acoscos  26859  atanlogaddlem  26879  atantayl2  26904  atantayl3  26905  birthdaylem2  26918  efrlim  26935  efrlimOLD  26936  amgmlem  26956  logdifbnd  26960  emcllem3  26964  emcllem6  26967  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem5  26999  gamigam  27019  lgamcvg2  27021  gamfac  27033  basellem3  27049  basellem8  27054  basellem9  27055  chtprm  27119  logfaclbnd  27189  perfect1  27195  bcp1ctr  27246  bclbnd  27247  bposlem1  27251  lgsdilem  27291  lgsdirnn0  27311  lgsdinn0  27312  gausslemma2dlem1a  27332  gausslemma2dlem4  27336  gausslemma2dlem5a  27337  lgseisenlem2  27343  lgsquadlem1  27347  2sqlem2  27385  mul2sq  27386  2sqmod  27403  2sqnn0  27405  vmadivsum  27449  rpvmasumlem  27454  dchrisumlem1  27456  dchrisumlem2  27457  dchrmusum2  27461  dchrvmasum2if  27464  dchrisum0lem2  27485  logsqvma2  27510  selberg3  27526  selberg4lem1  27527  pntrsumo1  27532  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntibndlem2  27558  pntlemk  27573  pntlemo  27574  ostth2lem4  27603  ostth3  27605  subsfo  28061  negsval2  28062  ltonold  28257  noseqrdgfn  28302  n0fincut  28351  addhalfcut  28455  bdayfinbndlem1  28463  z12shalf  28476  tgbtwndiff  28578  tgifscgr  28580  trgcgrg  28587  motcgr3  28617  tgbtwnconn1lem1  28644  tgbtwnconn1lem2  28645  ismir  28731  miriso  28742  midexlem  28764  ragmir  28772  footexALT  28790  footexlem1  28791  footexlem2  28792  colperpexlem3  28804  mideulem2  28806  midex  28809  opphllem3  28821  midcgr  28852  lmiisolem  28868  brbtwn2  28978  colinearalglem4  28982  axsegconlem1  28990  axpaschlem  29013  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  ushgredgedgloop  29304  crctcshwlkn0lem6  29888  wwlknlsw  29920  wwlksnextwrd  29970  clwlkclwwlklem2a3  30069  clwlkclwwlk2  30078  clwwlkel  30121  clwwlkfo  30125  clwwlkext2edg  30131  eupth2eucrct  30292  numclwwlk2lem1lem  30417  numclwwlk1lem2fo  30433  numclwlk2lem2f  30452  grpoidinvlem2  30580  nvmtri  30746  cnnvm  30757  nvnd  30763  ipidsq  30785  ipnm  30786  ipipcj  30790  blocnilem  30879  ipasslem2  30907  dipsubdir  30923  hvaddsubval  31108  pjhthlem1  31466  pjspansn  31652  pjo  31746  unoplin  31995  adjadj  32011  hmoplin  32017  eigvec1  32037  lnopeqi  32083  nmcexi  32101  lnfnsubi  32121  riesz3i  32137  kbass6  32196  leoprf2  32202  leoprf  32203  pjnmopi  32223  mdslmd1lem1  32400  mdslmd1lem2  32401  superpos  32429  ifeq3da  32621  fresunsn  32703  fgreu  32750  cocnvf1o  32808  resf1o  32809  quad3d  32829  fprodex01  32906  sgnmul  32916  ccatws1f1o  33033  wrdt2ind  33035  mndlactfo  33109  mndractfo  33111  gsummpt2d  33132  gsummptp1  33140  xrge0tsmseq  33157  gsumwrd2dccatlem  33159  gsumwrd2dccat  33160  symgfcoeu  33164  wrdpmtrlast  33175  psgnfzto1stlem  33182  psgnfzto1st  33187  cycpm2tr  33201  cycpmco2lem6  33213  cycpmco2lem7  33214  subrgchr  33319  elrgspnlem1  33324  elrgspnlem3  33326  elrgspnsubrunlem1  33329  rloccring  33352  rhmdvd  33405  qusrn  33490  nsgqusf1olem3  33496  rhmquskerlem  33506  elrspunsn  33510  mxidlirredi  33552  qsdrngi  33576  1arithidomlem1  33616  1arithidomlem2  33617  evls1subd  33653  deg1prod  33664  r1pid2OLD  33690  evlextv  33707  esplyind  33731  esplyindfv  33732  esplyfvn  33733  vietalem  33735  resssra  33743  dimval  33757  dimvalfi  33758  lindsunlem  33781  dimkerim  33784  qusdimsum  33785  fedgmullem1  33786  extdg1id  33823  fldextrspunlsplem  33830  fldextrspunlsp  33831  fldextrspunlem1  33832  fldextrspundgdvds  33838  extdgfialglem1  33849  extdgfialglem2  33850  ply1annidllem  33858  algextdeglem4  33877  constrrtcc  33892  constrsslem  33898  constrresqrtcl  33934  cos9thpiminplylem2  33940  cos9thpiminply  33945  madjusmdetlem2  33985  qtophaus  33993  zarclssn  34030  zarcmplem  34038  pstmval  34052  mndpluscn  34083  qqhucn  34149  esumval  34203  gsumesum  34216  esumcst  34220  esumpcvgval  34235  oddpwdc  34511  eulerpartlemgvv  34533  probdif  34577  signsvtn  34741  actfunsnf1o  34761  reprpmtf1o  34783  hgt750lemd  34805  logdivsqrle  34807  hgt750lemg  34811  hgt750lemb  34813  bnj1415  35194  swrdrevpfx  35311  pfxwlk  35318  derangen2  35368  subfaclefac  35370  subfaclim  35382  satom  35550  fmla  35575  mrsubrn  35707  sinccvglem  35866  bcprod  35932  filnetlem4  36575  curunc  37803  ltflcei  37809  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem24  37845  mblfinlem4  37861  ibladdnclem  37877  iblabsnc  37885  iblmulc2nc  37886  ftc1anclem6  37899  ftc1anclem8  37901  sdclem2  37943  ismtycnv  38003  heiborlem10  38021  lflvsass  39341  lkrscss  39358  eqlkr  39359  eqlkr3  39361  ldualvsdi2  39404  omllaw3  39505  cmtcomlemN  39508  cmtbr3N  39514  omlfh3N  39519  llnexchb2lem  40128  dalawlem7  40137  dalawlem11  40141  dalawlem12  40142  pol1N  40170  paddatclN  40209  4atexlemcnd  40332  ltrncoidN  40388  cdleme3b  40489  cdleme11  40530  cdleme15a  40534  cdleme22e  40604  cdleme22g  40608  cdlemg18b  40939  trlcoat  40983  cdlemk2  41092  cdlemk4  41094  cdlemki  41101  cdlemksv2  41107  cdlemk15  41115  cdlemk55a  41219  diainN  41317  dia2dimlem3  41326  dia2dimlem5  41328  dvhlveclem  41368  diaocN  41385  cdlemn4  41458  cdlemn8  41464  dihopelvalcpre  41508  dihmeetlem9N  41575  dih1dimatlem  41589  dihpN  41596  dochvalr3  41623  dochsat  41643  djhjlj  41663  dochdmm1  41670  dihjatcclem4  41681  dihjat1  41689  dihjat4  41693  dochsnkr2cl  41734  dochfl1  41736  lclkrlem2j  41776  mapdordlem2  41897  mapdrvallem2  41905  hdmap10  42100  lcmineqlem12  42294  3lexlogpow5ineq5  42314  aks4d1p1  42330  primrootsunit1  42351  primrootscoprmpow  42353  posbezout  42354  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p7  42367  evl1gprodd  42371  hashscontpow1  42375  aks6d1c3  42377  aks6d1c2lem3  42380  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem3  42391  aks6d1c6lem1  42424  aks6d1c6isolem3  42430  aks6d1c6lem5  42431  bcle2d  42433  aks6d1c7lem1  42434  aks5lem3a  42443  grpods  42448  unitscyglem1  42449  unitscyglem2  42450  unitscyglem4  42452  unitscyglem5  42453  aks5lem7  42454  nicomachus  42567  sumcubes  42568  cnreeu  42745  frlmvscadiccat  42761  grpcominv1  42763  riccrng1  42776  ricdrng1  42783  frlmsnic  42795  evlselv  42830  fsuppind  42833  flt4lem7  42902  negexpidd  42924  3cubeslem2  42927  3cubeslem3r  42929  mzpsubmpt  42985  irrapxlem3  43066  pellexlem6  43076  pell1234qrne0  43095  pell1234qrreccl  43096  pell1234qrmulcl  43097  pell14qrdich  43111  pell1qrgaplem  43115  rmxluc  43178  rmyluc  43179  jm2.24nn  43201  jm2.18  43230  jm2.19lem2  43232  jm2.19lem3  43233  jm2.22  43237  jm2.23  43238  jm2.16nn0  43246  jm2.27c  43249  fnwe2lem2  43293  lmhmfgsplit  43328  hbtlem2  43366  onsucf1lem  43511  ofoafo  43598  naddcnffo  43606  naddwordnexlem4  43643  reabssgn  43877  relexpmulnn  43950  relexpmulg  43951  ntrclsneine0lem  44305  int-addassocd  44415  dvconstbi  44575  bccm1k  44583  binomcxplemnotnn0  44597  fmptsnxp  45413  wessf1ornlem  45429  projf1o  45441  infnsuprnmpt  45494  lefldiveq  45540  lt4addmuld  45554  fzdifsuc2  45558  suplesup  45584  infrpge  45596  xrlexaddrp  45597  xralrple2  45599  infleinflem1  45614  supminfrnmpt  45689  supminfxr2  45713  fsumnncl  45818  limcperiod  45874  sumnnodd  45876  limcresiooub  45886  limcresioolb  45887  0ellimcdiv  45893  reclimc  45897  limsupval3  45936  limsupequzmpt2  45962  liminfval5  46009  limsupresxr  46010  liminfresxr  46011  liminfvalxr  46027  liminfequzmpt2  46035  climliminflimsupd  46045  liminfltlem  46048  liminflbuz2  46059  sinmulcos  46109  coskpi2  46110  cncfdmsn  46134  cncfiooicclem1  46137  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  fperdvper  46163  dvnmptdivc  46182  dvnxpaek  46186  dvnmul  46187  dvnprodlem1  46190  dvnprodlem3  46192  itgcoscmulx  46213  itgsincmulx  46218  itgspltprt  46223  itgiccshift  46224  itgperiod  46225  sublevolico  46228  volioof  46231  ovolsplit  46232  fvvolioof  46233  fvvolicof  46235  stoweidlem22  46266  stoweidlem32  46276  wallispilem5  46313  stirlinglem5  46322  dirkertrigeqlem2  46343  dirkertrigeq  46345  dirkercncflem1  46347  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem13  46364  fourierdlem16  46367  fourierdlem19  46370  fourierdlem21  46372  fourierdlem22  46373  fourierdlem28  46379  fourierdlem32  46383  fourierdlem33  46384  fourierdlem42  46393  fourierdlem47  46397  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem56  46406  fourierdlem60  46410  fourierdlem61  46411  fourierdlem64  46414  fourierdlem66  46416  fourierdlem71  46421  fourierdlem73  46423  fourierdlem74  46424  fourierdlem76  46426  fourierdlem78  46428  fourierdlem79  46429  fourierdlem80  46430  fourierdlem81  46431  fourierdlem83  46433  fourierdlem88  46438  fourierdlem92  46442  fourierdlem93  46443  fourierdlem97  46447  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem109  46459  fourierdlem111  46461  fouriersw  46475  elaa2lem  46477  etransclem24  46502  etransclem25  46503  etransclem35  46513  etransclem46  46524  rrndistlt  46534  rrxunitopnfi  46536  qndenserrnbl  46539  qndenserrnopnlem  46541  saldifcl2  46572  intsal  46574  sge0sn  46623  sge0ltfirp  46644  sge0iunmptlemre  46659  sge0fodjrnlem  46660  sge0isum  46671  sge0xaddlem1  46677  nnfoctbdjlem  46699  meassle  46707  ismeannd  46711  meadif  46723  meaiuninclem  46724  meaiininclem  46730  omeunile  46749  caragendifcl  46758  caratheodory  46772  isomenndlem  46774  ovnsubaddlem1  46814  hoidmv1lelem2  46836  hoidmv1le  46838  hoidmvlelem2  46840  hoidmvle  46844  hoi2toco  46851  rrnmbl  46858  hoidifhspdmvle  46864  voncmpl  46865  hoiqssbl  46869  hspmbllem1  46870  hspmbllem2  46871  ovolval2lem  46887  ovolval5lem2  46897  ovnovollem1  46900  ovnovollem2  46901  hoimbl2  46909  vonhoire  46916  salpreimagelt  46951  salpreimalegt  46953  preimaioomnf  46963  smfres  47034  smfmullem1  47035  smflimmpt  47054  smfsupmpt  47059  smfinfmpt  47063  smflimsupmpt  47073  smfliminflem  47074  smfliminfmpt  47076  sigarcol  47108  f1oresf1o  47536  elsprel  47721  prproropf1o  47753  paireqne  47757  sfprmdvdsmersenne  47849  lighneallem3  47853  lighneallem4  47856  nn0onn0exALTV  47945  nnsum3primesprm  48036  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  isuspgrim0lem  48139  clnbgrgrimlem  48179  uspgrlimlem3  48236  uspgrlimlem4  48237  gpgedgvtx0  48307  gpgedgvtx1  48308  funcringcsetcALTV2lem7  48542  funcringcsetclem7ALTV  48565  lincext3  48702  lincresunit3  48727  nn0onn0ex  48769  nnpw2pmod  48829  blennn0em1  48837  digexp  48853  dignn0ehalf  48863  nn0mulfsum  48870  itcovalpclem1  48916  eenglngeehlnmlem2  48984  rrx2vlinest  48987  line2  48998  itschlc0xyqsol  49013  itsclinecirc0b  49020  toplatjoin  49247  toplatmeet  49248  upeu2lem  49273  oppff1o  49394  imaf1co  49400  upciclem3  49413  natoppfb  49476  oppcthinco  49684  oppcthinendcALT  49686  lmddu  49912  recsec  50001  reccsc  50002  aacllem  50046  amgmlemALT  50048