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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  3eqtrrd  2776  3eqtr2rd  2778  ifan  4520  ifor  4521  dfopif  4813  fnco  6616  fnsnfv  6919  nvocnv  7236  elovmpt3rab1  7627  onsucmin  7772  csbopeq1a  8003  oaabs2  8585  ecinxp  8739  resixpfo  8884  sbthlem3  9027  rankxpsuc  9806  fseqenlem2  9947  dfac2b  10053  isf32lem9  10283  compsscnvlem  10292  ttukeylem7  10437  fpwwe2lem10  10563  00id  11321  submul2  11590  mulsubfacd  11611  divadddiv  11870  infrenegsup  12139  xadd4d  13255  fzdifsuc  13538  fzval3  13689  fzoshftral  13742  ceim1l  13806  fldiv  13819  flmod  13844  intfrac  13845  modcyc2  13866  modaddb  13868  moddi  13901  uzrdgfni  13920  axdc4uzlem  13945  seqf1olem1  14003  seqf1olem2  14004  seqid2  14010  expnegz  14058  binom2sub  14182  binom3  14186  hashreshashfun  14401  ccatw2s1p2  14600  ccats1pfxeq  14676  pfxccatin12lem2  14693  pfxccatin12  14695  swrdccat3b  14702  cshweqrep  14783  2cshwcshw  14787  ccatco  14797  swrds2  14902  relexpsucnnr  14987  relexpaddnn  15013  reim  15071  mulre  15083  addcj  15110  absimle  15271  clim2ser  15617  isercoll2  15631  serf0  15643  iseralt  15647  summolem3  15676  isumclim3  15721  mptfzshft  15740  fsumrev  15741  fsum2mul  15751  incexc  15802  isumsplit  15805  mertenslem1  15849  fprodrev  15942  iprodclim3  15965  binomfallfaclem2  16005  ef4p  16080  tanval3  16101  efival  16119  sinmul  16139  bitsinvp1  16418  sadaddlem  16435  bitsshft  16444  smu01lem  16454  dfgcd2  16515  lcmgcdlem  16575  lcm1  16579  lcmfass  16615  eulerthlem2  16752  hashgcdeq  16760  powm2modprm  16774  pythagtriplem16  16801  pczpre  16818  pcqdiv  16828  pcadd  16860  pcfac  16870  prmreclem5  16891  4sqlem10  16918  4sqlem19  16934  vdwapun  16945  vdwlem1  16952  ramcl  17000  setsstruct  17146  strfvd  17170  strfv2d  17171  xpsff1o  17531  xpsrnbas  17535  2oppccomf  17691  oppcepi  17706  sscfn1  17784  sscfn2  17785  invfuc  17944  funcestrcsetclem7  18112  funcsetcestrclem7  18127  gsumsplit1r  18655  grpinvssd  18993  grpinvval2  18999  cycsubggend  19180  pmtrdifwrdellem2  19457  psgnunilem1  19468  psgnuni  19474  pgp0  19571  sylow1lem1  19573  sylow3lem2  19603  efgredleme  19718  efgcpbllemb  19730  frgpuptinv  19746  frgpup3lem  19752  gexexlem  19827  cyggenod  19859  gsumval3eu  19879  gsumval3  19882  gsumzaddlem  19896  dprd2db  20020  ablsimpgfindlem1  20084  ringinvdv  20394  c0snmgmhm  20442  rngcifuestrc  20616  funcrngcsetc  20617  funcrngcsetcALT  20618  funcringcsetc  20651  lss1d  20958  pwssplit1  21054  rhmqusnsg  21283  rngqiprnglin  21300  znzrh2  21525  regsumsupp  21602  ipassr2  21627  dsmmfi  21718  frlmlss  21731  frlmip  21758  frlmlbs  21777  frlmup3  21780  islindf4  21818  mplcoe3  22016  subrgascl  22044  evlseu  22061  psdadd  22129  ply1sclid  22253  ply1chr  22271  evls1addd  22336  evls1muld  22337  evls1vsca  22338  evls1maprhm  22341  evls1maplmhm  22342  evls1maprnss  22343  evl1maprhm  22344  1marepvmarrepid  22540  madurid  22609  smadiadetlem3  22633  mat2pmatghm  22695  pmatcollpwscmatlem1  22754  pm2mpmhmlem2  22784  cpmadurid  22832  cpmidgsumm2pm  22834  cpmadugsumlemB  22839  cayhamlem2  22849  ntrval2  23016  ordtuni  23155  cnclima  23233  cmpsub  23365  ptbasfi  23546  txbasval  23571  pt1hmeo  23771  alexsubALTlem1  24012  trust  24194  ussid  24225  ressuss  24227  ressprdsds  24336  imasdsf1olem  24338  setsms  24445  tmsxms  24451  tmsxpsmopn  24502  subgnm  24598  tngnm  24616  tngngp2  24617  xrsxmet  24775  xrge0gsumle  24799  metdstri  24817  xrhmeo  24913  lebnumlem3  24930  pcorevlem  24993  pi1xfrcnvlem  25023  clmabs  25050  cvsmuleqdivd  25101  rrxip  25357  rrxds  25360  rrxdsfi  25378  minveclem4a  25397  pjthlem1  25404  divcncf  25414  ovolunlem1a  25463  mbfres2  25612  i1faddlem  25660  ibladdlem  25787  iblabs  25796  ditgsplit  25828  dvmptresicc  25883  dvnres  25898  dvmptdiv  25941  dveflem  25946  dveq0  25967  dvfsumabs  25990  itgsubstlem  26015  ply1divex  26102  r1pid2  26127  dgrco  26240  plycjlem  26241  taylthlem1  26338  pserdv2  26395  abelthlem6  26401  abelthlem7  26403  tangtx  26469  abssinper  26485  sineq0  26488  explog  26558  reexplog  26559  eflogeq  26566  abslogle  26582  tanarg  26583  logtayl  26624  logtayl2  26626  relogbdiv  26743  ang180lem3  26775  affineequiv  26787  affineequiv2  26788  chordthmlem4  26799  chordthmlem5  26800  heron  26802  dcubic1lem  26807  dcubic2  26808  dcubic  26810  mcubic  26811  cubic2  26812  dquartlem1  26815  dquart  26817  quart1lem  26819  quartlem1  26821  quart  26825  acoscos  26857  atanlogaddlem  26877  atantayl2  26902  atantayl3  26903  birthdaylem2  26916  efrlim  26933  amgmlem  26953  logdifbnd  26957  emcllem3  26961  emcllem6  26964  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  gamigam  27016  lgamcvg2  27018  gamfac  27030  basellem3  27046  basellem8  27051  basellem9  27052  chtprm  27116  logfaclbnd  27185  perfect1  27191  bcp1ctr  27242  bclbnd  27243  bposlem1  27247  lgsdilem  27287  lgsdirnn0  27307  lgsdinn0  27308  gausslemma2dlem1a  27328  gausslemma2dlem4  27332  gausslemma2dlem5a  27333  lgseisenlem2  27339  lgsquadlem1  27343  2sqlem2  27381  mul2sq  27382  2sqmod  27399  2sqnn0  27401  vmadivsum  27445  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem2  27453  dchrmusum2  27457  dchrvmasum2if  27460  dchrisum0lem2  27481  logsqvma2  27506  selberg3  27522  selberg4lem1  27523  pntrsumo1  27528  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem5  27544  pntibndlem2  27554  pntlemk  27569  pntlemo  27570  ostth2lem4  27599  ostth3  27601  subsfo  28057  negsval2  28058  ltonold  28253  noseqrdgfn  28298  n0fincut  28347  addhalfcut  28451  bdayfinbndlem1  28459  z12shalf  28472  tgbtwndiff  28574  tgifscgr  28576  trgcgrg  28583  motcgr3  28613  tgbtwnconn1lem1  28640  tgbtwnconn1lem2  28641  ismir  28727  miriso  28738  midexlem  28760  ragmir  28768  footexALT  28786  footexlem1  28787  footexlem2  28788  colperpexlem3  28800  mideulem2  28802  midex  28805  opphllem3  28817  midcgr  28848  lmiisolem  28864  brbtwn2  28974  colinearalglem4  28978  axsegconlem1  28986  axpaschlem  29009  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  ushgredgedgloop  29300  crctcshwlkn0lem6  29883  wwlknlsw  29915  wwlksnextwrd  29965  clwlkclwwlklem2a3  30064  clwlkclwwlk2  30073  clwwlkel  30116  clwwlkfo  30120  clwwlkext2edg  30126  eupth2eucrct  30287  numclwwlk2lem1lem  30412  numclwwlk1lem2fo  30428  numclwlk2lem2f  30447  grpoidinvlem2  30576  nvmtri  30742  cnnvm  30753  nvnd  30759  ipidsq  30781  ipnm  30782  ipipcj  30786  blocnilem  30875  ipasslem2  30903  dipsubdir  30919  hvaddsubval  31104  pjhthlem1  31462  pjspansn  31648  pjo  31742  unoplin  31991  adjadj  32007  hmoplin  32013  eigvec1  32033  lnopeqi  32079  nmcexi  32097  lnfnsubi  32117  riesz3i  32133  kbass6  32192  leoprf2  32198  leoprf  32199  pjnmopi  32219  mdslmd1lem1  32396  mdslmd1lem2  32397  superpos  32425  ifeq3da  32616  fresunsn  32698  fgreu  32744  cocnvf1o  32802  resf1o  32803  quad3d  32822  fprodex01  32898  sgnmul  32908  ccatws1f1o  33011  wrdt2ind  33013  mndlactfo  33087  mndractfo  33089  gsummpt2d  33110  gsummptp1  33118  xrge0tsmseq  33136  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  symgfcoeu  33143  wrdpmtrlast  33154  psgnfzto1stlem  33161  psgnfzto1st  33166  cycpm2tr  33180  cycpmco2lem6  33192  cycpmco2lem7  33193  subrgchr  33298  elrgspnlem1  33303  elrgspnlem3  33305  elrgspnsubrunlem1  33308  rloccring  33331  rhmdvd  33384  qusrn  33469  nsgqusf1olem3  33475  rhmquskerlem  33485  elrspunsn  33489  mxidlirredi  33531  qsdrngi  33555  1arithidomlem1  33595  1arithidomlem2  33596  evls1subd  33632  deg1prod  33643  r1pid2OLD  33669  evlextv  33686  psrmonprod  33696  esplyfval1  33717  esplyind  33719  esplyindfv  33720  esplyfvn  33721  vietalem  33723  resssra  33731  dimval  33745  dimvalfi  33746  lindsunlem  33768  dimkerim  33771  qusdimsum  33772  fedgmullem1  33773  extdg1id  33810  fldextrspunlsplem  33817  fldextrspunlsp  33818  fldextrspunlem1  33819  fldextrspundgdvds  33825  extdgfialglem1  33836  extdgfialglem2  33837  ply1annidllem  33845  algextdeglem4  33864  constrrtcc  33879  constrsslem  33885  constrresqrtcl  33921  cos9thpiminplylem2  33927  cos9thpiminply  33932  madjusmdetlem2  33972  qtophaus  33980  zarclssn  34017  zarcmplem  34025  pstmval  34039  mndpluscn  34070  qqhucn  34136  esumval  34190  gsumesum  34203  esumcst  34207  esumpcvgval  34222  oddpwdc  34498  eulerpartlemgvv  34520  probdif  34564  signsvtn  34728  actfunsnf1o  34748  reprpmtf1o  34770  hgt750lemd  34792  logdivsqrle  34794  hgt750lemg  34798  hgt750lemb  34800  bnj1415  35180  swrdrevpfx  35299  pfxwlk  35306  derangen2  35356  subfaclefac  35358  subfaclim  35370  satom  35538  fmla  35563  mrsubrn  35695  sinccvglem  35854  bcprod  35920  filnetlem4  36563  curunc  37923  ltflcei  37929  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  mblfinlem4  37981  ibladdnclem  37997  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem6  38019  ftc1anclem8  38021  sdclem2  38063  ismtycnv  38123  heiborlem10  38141  lflvsass  39527  lkrscss  39544  eqlkr  39545  eqlkr3  39547  ldualvsdi2  39590  omllaw3  39691  cmtcomlemN  39694  cmtbr3N  39700  omlfh3N  39705  llnexchb2lem  40314  dalawlem7  40323  dalawlem11  40327  dalawlem12  40328  pol1N  40356  paddatclN  40395  4atexlemcnd  40518  ltrncoidN  40574  cdleme3b  40675  cdleme11  40716  cdleme15a  40720  cdleme22e  40790  cdleme22g  40794  cdlemg18b  41125  trlcoat  41169  cdlemk2  41278  cdlemk4  41280  cdlemki  41287  cdlemksv2  41293  cdlemk15  41301  cdlemk55a  41405  diainN  41503  dia2dimlem3  41512  dia2dimlem5  41514  dvhlveclem  41554  diaocN  41571  cdlemn4  41644  cdlemn8  41650  dihopelvalcpre  41694  dihmeetlem9N  41761  dih1dimatlem  41775  dihpN  41782  dochvalr3  41809  dochsat  41829  djhjlj  41849  dochdmm1  41856  dihjatcclem4  41867  dihjat1  41875  dihjat4  41879  dochsnkr2cl  41920  dochfl1  41922  lclkrlem2j  41962  mapdordlem2  42083  mapdrvallem2  42091  hdmap10  42286  lcmineqlem12  42479  3lexlogpow5ineq5  42499  aks4d1p1  42515  primrootsunit1  42536  primrootscoprmpow  42538  posbezout  42539  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p7  42552  evl1gprodd  42556  hashscontpow1  42560  aks6d1c3  42562  aks6d1c2lem3  42565  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem3  42576  aks6d1c6lem1  42609  aks6d1c6isolem3  42615  aks6d1c6lem5  42616  bcle2d  42618  aks6d1c7lem1  42619  aks5lem3a  42628  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  aks5lem7  42639  nicomachus  42744  sumcubes  42745  cnreeu  42935  frlmvscadiccat  42951  grpcominv1  42953  riccrng1  42966  ricdrng1  42973  frlmsnic  42985  evlselv  43020  fsuppind  43023  flt4lem7  43092  negexpidd  43114  3cubeslem2  43117  3cubeslem3r  43119  mzpsubmpt  43175  irrapxlem3  43252  pellexlem6  43262  pell1234qrne0  43281  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell14qrdich  43297  pell1qrgaplem  43301  rmxluc  43364  rmyluc  43365  jm2.24nn  43387  jm2.18  43416  jm2.19lem2  43418  jm2.19lem3  43419  jm2.22  43423  jm2.23  43424  jm2.16nn0  43432  jm2.27c  43435  fnwe2lem2  43479  lmhmfgsplit  43514  hbtlem2  43552  onsucf1lem  43697  ofoafo  43784  naddcnffo  43792  naddwordnexlem4  43829  reabssgn  44063  relexpmulnn  44136  relexpmulg  44137  ntrclsneine0lem  44491  int-addassocd  44601  dvconstbi  44761  bccm1k  44769  binomcxplemnotnn0  44783  fmptsnxp  45599  wessf1ornlem  45615  projf1o  45626  infnsuprnmpt  45679  lefldiveq  45725  lt4addmuld  45739  fzdifsuc2  45743  suplesup  45769  infrpge  45781  xrlexaddrp  45782  xralrple2  45784  infleinflem1  45799  supminfrnmpt  45873  supminfxr2  45897  fsumnncl  46002  limcperiod  46058  sumnnodd  46060  limcresiooub  46070  limcresioolb  46071  0ellimcdiv  46077  reclimc  46081  limsupval3  46120  limsupequzmpt2  46146  liminfval5  46193  limsupresxr  46194  liminfresxr  46195  liminfvalxr  46211  liminfequzmpt2  46219  climliminflimsupd  46229  liminfltlem  46232  liminflbuz2  46243  sinmulcos  46293  coskpi2  46294  cncfdmsn  46318  cncfiooicclem1  46321  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  fperdvper  46347  dvnmptdivc  46366  dvnxpaek  46370  dvnmul  46371  dvnprodlem1  46374  dvnprodlem3  46376  itgcoscmulx  46397  itgsincmulx  46402  itgspltprt  46407  itgiccshift  46408  itgperiod  46409  sublevolico  46412  volioof  46415  ovolsplit  46416  fvvolioof  46417  fvvolicof  46419  stoweidlem22  46450  stoweidlem32  46460  wallispilem5  46497  stirlinglem5  46506  dirkertrigeqlem2  46527  dirkertrigeq  46529  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem13  46548  fourierdlem16  46551  fourierdlem19  46554  fourierdlem21  46556  fourierdlem22  46557  fourierdlem28  46563  fourierdlem32  46567  fourierdlem33  46568  fourierdlem42  46577  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem56  46590  fourierdlem60  46594  fourierdlem61  46595  fourierdlem64  46598  fourierdlem66  46600  fourierdlem71  46605  fourierdlem73  46607  fourierdlem74  46608  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem80  46614  fourierdlem81  46615  fourierdlem83  46617  fourierdlem88  46622  fourierdlem92  46626  fourierdlem93  46627  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem109  46643  fourierdlem111  46645  fouriersw  46659  elaa2lem  46661  etransclem24  46686  etransclem25  46687  etransclem35  46697  etransclem46  46708  rrndistlt  46718  rrxunitopnfi  46720  qndenserrnbl  46723  qndenserrnopnlem  46725  saldifcl2  46756  intsal  46758  sge0sn  46807  sge0ltfirp  46828  sge0iunmptlemre  46843  sge0fodjrnlem  46844  sge0isum  46855  sge0xaddlem1  46861  nnfoctbdjlem  46883  meassle  46891  ismeannd  46895  meadif  46907  meaiuninclem  46908  meaiininclem  46914  omeunile  46933  caragendifcl  46942  caratheodory  46956  isomenndlem  46958  ovnsubaddlem1  46998  hoidmv1lelem2  47020  hoidmv1le  47022  hoidmvlelem2  47024  hoidmvle  47028  hoi2toco  47035  rrnmbl  47042  hoidifhspdmvle  47048  voncmpl  47049  hoiqssbl  47053  hspmbllem1  47054  hspmbllem2  47055  ovolval2lem  47071  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  hoimbl2  47093  vonhoire  47100  salpreimagelt  47135  salpreimalegt  47137  preimaioomnf  47147  smfres  47218  smfmullem1  47219  smflimmpt  47238  smfsupmpt  47243  smfinfmpt  47247  smflimsupmpt  47257  smfliminflem  47258  smfliminfmpt  47260  sigarcol  47292  sin5tlem2  47322  f1oresf1o  47738  elsprel  47935  prproropf1o  47967  paireqne  47971  sfprmdvdsmersenne  48066  lighneallem3  48070  lighneallem4  48073  nprmdvdsfacm1lem1  48083  nn0onn0exALTV  48175  nnsum3primesprm  48266  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  isuspgrim0lem  48369  clnbgrgrimlem  48409  uspgrlimlem3  48466  uspgrlimlem4  48467  gpgedgvtx0  48537  gpgedgvtx1  48538  funcringcsetcALTV2lem7  48772  funcringcsetclem7ALTV  48795  lincext3  48932  lincresunit3  48957  nn0onn0ex  48999  nnpw2pmod  49059  blennn0em1  49067  digexp  49083  dignn0ehalf  49093  nn0mulfsum  49100  itcovalpclem1  49146  eenglngeehlnmlem2  49214  rrx2vlinest  49217  line2  49228  itschlc0xyqsol  49243  itsclinecirc0b  49250  toplatjoin  49477  toplatmeet  49478  upeu2lem  49503  oppff1o  49624  imaf1co  49630  upciclem3  49643  natoppfb  49706  oppcthinco  49914  oppcthinendcALT  49916  lmddu  50142  recsec  50231  reccsc  50232  aacllem  50276  amgmlemALT  50278