Theorem eqtr2d 2773

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 2772	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2743	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 2709

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

This theorem is referenced by:  3eqtrrd  2777  3eqtr2rd  2779  ifan  4521  ifor  4522  dfopif  4814  fnco  6610  fnsnfv  6913  nvocnv  7229  elovmpt3rab1  7620  onsucmin  7765  csbopeq1a  7996  oaabs2  8578  ecinxp  8732  resixpfo  8877  sbthlem3  9020  rankxpsuc  9797  fseqenlem2  9938  dfac2b  10044  isf32lem9  10274  compsscnvlem  10283  ttukeylem7  10428  fpwwe2lem10  10554  00id  11312  submul2  11581  mulsubfacd  11602  divadddiv  11861  infrenegsup  12130  xadd4d  13246  fzdifsuc  13529  fzval3  13680  fzoshftral  13733  ceim1l  13797  fldiv  13810  flmod  13835  intfrac  13836  modcyc2  13857  modaddb  13859  moddi  13892  uzrdgfni  13911  axdc4uzlem  13936  seqf1olem1  13994  seqf1olem2  13995  seqid2  14001  expnegz  14049  binom2sub  14173  binom3  14177  hashreshashfun  14392  ccatw2s1p2  14591  ccats1pfxeq  14667  pfxccatin12lem2  14684  pfxccatin12  14686  swrdccat3b  14693  cshweqrep  14774  2cshwcshw  14778  ccatco  14788  swrds2  14893  relexpsucnnr  14978  relexpaddnn  15004  reim  15062  mulre  15074  addcj  15101  absimle  15262  clim2ser  15608  isercoll2  15622  serf0  15634  iseralt  15638  summolem3  15667  isumclim3  15712  mptfzshft  15731  fsumrev  15732  fsum2mul  15742  incexc  15793  isumsplit  15796  mertenslem1  15840  fprodrev  15933  iprodclim3  15956  binomfallfaclem2  15996  ef4p  16071  tanval3  16092  efival  16110  sinmul  16130  bitsinvp1  16409  sadaddlem  16426  bitsshft  16435  smu01lem  16445  dfgcd2  16506  lcmgcdlem  16566  lcm1  16570  lcmfass  16606  eulerthlem2  16743  hashgcdeq  16751  powm2modprm  16765  pythagtriplem16  16792  pczpre  16809  pcqdiv  16819  pcadd  16851  pcfac  16861  prmreclem5  16882  4sqlem10  16909  4sqlem19  16925  vdwapun  16936  vdwlem1  16943  ramcl  16991  setsstruct  17137  strfvd  17161  strfv2d  17162  xpsff1o  17522  xpsrnbas  17526  2oppccomf  17682  oppcepi  17697  sscfn1  17775  sscfn2  17776  invfuc  17935  funcestrcsetclem7  18103  funcsetcestrclem7  18118  gsumsplit1r  18646  grpinvssd  18984  grpinvval2  18990  cycsubggend  19171  pmtrdifwrdellem2  19448  psgnunilem1  19459  psgnuni  19465  pgp0  19562  sylow1lem1  19564  sylow3lem2  19594  efgredleme  19709  efgcpbllemb  19721  frgpuptinv  19737  frgpup3lem  19743  gexexlem  19818  cyggenod  19850  gsumval3eu  19870  gsumval3  19873  gsumzaddlem  19887  dprd2db  20011  ablsimpgfindlem1  20075  ringinvdv  20385  c0snmgmhm  20433  rngcifuestrc  20607  funcrngcsetc  20608  funcrngcsetcALT  20609  funcringcsetc  20642  lss1d  20949  pwssplit1  21046  rhmqusnsg  21275  rngqiprnglin  21292  znzrh2  21535  regsumsupp  21612  ipassr2  21637  dsmmfi  21728  frlmlss  21741  frlmip  21768  frlmlbs  21787  frlmup3  21790  islindf4  21828  mplcoe3  22026  subrgascl  22054  evlseu  22071  psdadd  22139  ply1sclid  22263  ply1chr  22281  evls1addd  22346  evls1muld  22347  evls1vsca  22348  evls1maprhm  22351  evls1maplmhm  22352  evls1maprnss  22353  evl1maprhm  22354  1marepvmarrepid  22550  madurid  22619  smadiadetlem3  22643  mat2pmatghm  22705  pmatcollpwscmatlem1  22764  pm2mpmhmlem2  22794  cpmadurid  22842  cpmidgsumm2pm  22844  cpmadugsumlemB  22849  cayhamlem2  22859  ntrval2  23026  ordtuni  23165  cnclima  23243  cmpsub  23375  ptbasfi  23556  txbasval  23581  pt1hmeo  23781  alexsubALTlem1  24022  trust  24204  ussid  24235  ressuss  24237  ressprdsds  24346  imasdsf1olem  24348  setsms  24455  tmsxms  24461  tmsxpsmopn  24512  subgnm  24608  tngnm  24626  tngngp2  24627  xrsxmet  24785  xrge0gsumle  24809  metdstri  24827  xrhmeo  24923  lebnumlem3  24940  pcorevlem  25003  pi1xfrcnvlem  25033  clmabs  25060  cvsmuleqdivd  25111  rrxip  25367  rrxds  25370  rrxdsfi  25388  minveclem4a  25407  pjthlem1  25414  divcncf  25424  ovolunlem1a  25473  mbfres2  25622  i1faddlem  25670  ibladdlem  25797  iblabs  25806  ditgsplit  25838  dvmptresicc  25893  dvnres  25908  dvmptdiv  25951  dveflem  25956  dveq0  25977  dvfsumabs  26000  itgsubstlem  26025  ply1divex  26112  r1pid2  26137  dgrco  26250  plycjlem  26251  taylthlem1  26350  pserdv2  26408  abelthlem6  26414  abelthlem7  26416  tangtx  26482  abssinper  26498  sineq0  26501  explog  26571  reexplog  26572  eflogeq  26579  abslogle  26595  tanarg  26596  logtayl  26637  logtayl2  26639  relogbdiv  26756  ang180lem3  26788  affineequiv  26800  affineequiv2  26801  chordthmlem4  26812  chordthmlem5  26813  heron  26815  dcubic1lem  26820  dcubic2  26821  dcubic  26823  mcubic  26824  cubic2  26825  dquartlem1  26828  dquart  26830  quart1lem  26832  quartlem1  26834  quart  26838  acoscos  26870  atanlogaddlem  26890  atantayl2  26915  atantayl3  26916  birthdaylem2  26929  efrlim  26946  efrlimOLD  26947  amgmlem  26967  logdifbnd  26971  emcllem3  26975  emcllem6  26978  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem5  27010  gamigam  27030  lgamcvg2  27032  gamfac  27044  basellem3  27060  basellem8  27065  basellem9  27066  chtprm  27130  logfaclbnd  27199  perfect1  27205  bcp1ctr  27256  bclbnd  27257  bposlem1  27261  lgsdilem  27301  lgsdirnn0  27321  lgsdinn0  27322  gausslemma2dlem1a  27342  gausslemma2dlem4  27346  gausslemma2dlem5a  27347  lgseisenlem2  27353  lgsquadlem1  27357  2sqlem2  27395  mul2sq  27396  2sqmod  27413  2sqnn0  27415  vmadivsum  27459  rpvmasumlem  27464  dchrisumlem1  27466  dchrisumlem2  27467  dchrmusum2  27471  dchrvmasum2if  27474  dchrisum0lem2  27495  logsqvma2  27520  selberg3  27536  selberg4lem1  27537  pntrsumo1  27542  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem5  27558  pntibndlem2  27568  pntlemk  27583  pntlemo  27584  ostth2lem4  27613  ostth3  27615  subsfo  28071  negsval2  28072  ltonold  28267  noseqrdgfn  28312  n0fincut  28361  addhalfcut  28465  bdayfinbndlem1  28473  z12shalf  28486  tgbtwndiff  28588  tgifscgr  28590  trgcgrg  28597  motcgr3  28627  tgbtwnconn1lem1  28654  tgbtwnconn1lem2  28655  ismir  28741  miriso  28752  midexlem  28774  ragmir  28782  footexALT  28800  footexlem1  28801  footexlem2  28802  colperpexlem3  28814  mideulem2  28816  midex  28819  opphllem3  28831  midcgr  28862  lmiisolem  28878  brbtwn2  28988  colinearalglem4  28992  axsegconlem1  29000  axpaschlem  29023  axcontlem4  29050  axcontlem7  29053  axcontlem8  29054  ushgredgedgloop  29314  crctcshwlkn0lem6  29898  wwlknlsw  29930  wwlksnextwrd  29980  clwlkclwwlklem2a3  30079  clwlkclwwlk2  30088  clwwlkel  30131  clwwlkfo  30135  clwwlkext2edg  30141  eupth2eucrct  30302  numclwwlk2lem1lem  30427  numclwwlk1lem2fo  30443  numclwlk2lem2f  30462  grpoidinvlem2  30591  nvmtri  30757  cnnvm  30768  nvnd  30774  ipidsq  30796  ipnm  30797  ipipcj  30801  blocnilem  30890  ipasslem2  30918  dipsubdir  30934  hvaddsubval  31119  pjhthlem1  31477  pjspansn  31663  pjo  31757  unoplin  32006  adjadj  32022  hmoplin  32028  eigvec1  32048  lnopeqi  32094  nmcexi  32112  lnfnsubi  32132  riesz3i  32148  kbass6  32207  leoprf2  32213  leoprf  32214  pjnmopi  32234  mdslmd1lem1  32411  mdslmd1lem2  32412  superpos  32440  ifeq3da  32631  fresunsn  32713  fgreu  32759  cocnvf1o  32817  resf1o  32818  quad3d  32837  fprodex01  32913  sgnmul  32923  ccatws1f1o  33026  wrdt2ind  33028  mndlactfo  33102  mndractfo  33104  gsummpt2d  33125  gsummptp1  33133  xrge0tsmseq  33151  gsumwrd2dccatlem  33153  gsumwrd2dccat  33154  symgfcoeu  33158  wrdpmtrlast  33169  psgnfzto1stlem  33176  psgnfzto1st  33181  cycpm2tr  33195  cycpmco2lem6  33207  cycpmco2lem7  33208  subrgchr  33313  elrgspnlem1  33318  elrgspnlem3  33320  elrgspnsubrunlem1  33323  rloccring  33346  rhmdvd  33399  qusrn  33484  nsgqusf1olem3  33490  rhmquskerlem  33500  elrspunsn  33504  mxidlirredi  33546  qsdrngi  33570  1arithidomlem1  33610  1arithidomlem2  33611  evls1subd  33647  deg1prod  33658  r1pid2OLD  33684  evlextv  33701  psrmonprod  33711  esplyfval1  33732  esplyind  33734  esplyindfv  33735  esplyfvn  33736  vietalem  33738  resssra  33746  dimval  33760  dimvalfi  33761  lindsunlem  33784  dimkerim  33787  qusdimsum  33788  fedgmullem1  33789  extdg1id  33826  fldextrspunlsplem  33833  fldextrspunlsp  33834  fldextrspunlem1  33835  fldextrspundgdvds  33841  extdgfialglem1  33852  extdgfialglem2  33853  ply1annidllem  33861  algextdeglem4  33880  constrrtcc  33895  constrsslem  33901  constrresqrtcl  33937  cos9thpiminplylem2  33943  cos9thpiminply  33948  madjusmdetlem2  33988  qtophaus  33996  zarclssn  34033  zarcmplem  34041  pstmval  34055  mndpluscn  34086  qqhucn  34152  esumval  34206  gsumesum  34219  esumcst  34223  esumpcvgval  34238  oddpwdc  34514  eulerpartlemgvv  34536  probdif  34580  signsvtn  34744  actfunsnf1o  34764  reprpmtf1o  34786  hgt750lemd  34808  logdivsqrle  34810  hgt750lemg  34814  hgt750lemb  34816  bnj1415  35196  swrdrevpfx  35315  pfxwlk  35322  derangen2  35372  subfaclefac  35374  subfaclim  35386  satom  35554  fmla  35579  mrsubrn  35711  sinccvglem  35870  bcprod  35936  filnetlem4  36579  curunc  37937  ltflcei  37943  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem24  37979  mblfinlem4  37995  ibladdnclem  38011  iblabsnc  38019  iblmulc2nc  38020  ftc1anclem6  38033  ftc1anclem8  38035  sdclem2  38077  ismtycnv  38137  heiborlem10  38155  lflvsass  39541  lkrscss  39558  eqlkr  39559  eqlkr3  39561  ldualvsdi2  39604  omllaw3  39705  cmtcomlemN  39708  cmtbr3N  39714  omlfh3N  39719  llnexchb2lem  40328  dalawlem7  40337  dalawlem11  40341  dalawlem12  40342  pol1N  40370  paddatclN  40409  4atexlemcnd  40532  ltrncoidN  40588  cdleme3b  40689  cdleme11  40730  cdleme15a  40734  cdleme22e  40804  cdleme22g  40808  cdlemg18b  41139  trlcoat  41183  cdlemk2  41292  cdlemk4  41294  cdlemki  41301  cdlemksv2  41307  cdlemk15  41315  cdlemk55a  41419  diainN  41517  dia2dimlem3  41526  dia2dimlem5  41528  dvhlveclem  41568  diaocN  41585  cdlemn4  41658  cdlemn8  41664  dihopelvalcpre  41708  dihmeetlem9N  41775  dih1dimatlem  41789  dihpN  41796  dochvalr3  41823  dochsat  41843  djhjlj  41863  dochdmm1  41870  dihjatcclem4  41881  dihjat1  41889  dihjat4  41893  dochsnkr2cl  41934  dochfl1  41936  lclkrlem2j  41976  mapdordlem2  42097  mapdrvallem2  42105  hdmap10  42300  lcmineqlem12  42493  3lexlogpow5ineq5  42513  aks4d1p1  42529  primrootsunit1  42550  primrootscoprmpow  42552  posbezout  42553  aks6d1c1p3  42563  aks6d1c1p4  42564  aks6d1c1p5  42565  aks6d1c1p7  42566  evl1gprodd  42570  hashscontpow1  42574  aks6d1c3  42576  aks6d1c2lem3  42579  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5lem3  42590  aks6d1c6lem1  42623  aks6d1c6isolem3  42629  aks6d1c6lem5  42630  bcle2d  42632  aks6d1c7lem1  42633  aks5lem3a  42642  grpods  42647  unitscyglem1  42648  unitscyglem2  42649  unitscyglem4  42651  unitscyglem5  42652  aks5lem7  42653  nicomachus  42758  sumcubes  42759  cnreeu  42949  frlmvscadiccat  42965  grpcominv1  42967  riccrng1  42980  ricdrng1  42987  frlmsnic  42999  evlselv  43034  fsuppind  43037  flt4lem7  43106  negexpidd  43128  3cubeslem2  43131  3cubeslem3r  43133  mzpsubmpt  43189  irrapxlem3  43270  pellexlem6  43280  pell1234qrne0  43299  pell1234qrreccl  43300  pell1234qrmulcl  43301  pell14qrdich  43315  pell1qrgaplem  43319  rmxluc  43382  rmyluc  43383  jm2.24nn  43405  jm2.18  43434  jm2.19lem2  43436  jm2.19lem3  43437  jm2.22  43441  jm2.23  43442  jm2.16nn0  43450  jm2.27c  43453  fnwe2lem2  43497  lmhmfgsplit  43532  hbtlem2  43570  onsucf1lem  43715  ofoafo  43802  naddcnffo  43810  naddwordnexlem4  43847  reabssgn  44081  relexpmulnn  44154  relexpmulg  44155  ntrclsneine0lem  44509  int-addassocd  44619  dvconstbi  44779  bccm1k  44787  binomcxplemnotnn0  44801  fmptsnxp  45617  wessf1ornlem  45633  projf1o  45644  infnsuprnmpt  45697  lefldiveq  45743  lt4addmuld  45757  fzdifsuc2  45761  suplesup  45787  infrpge  45799  xrlexaddrp  45800  xralrple2  45802  infleinflem1  45817  supminfrnmpt  45891  supminfxr2  45915  fsumnncl  46020  limcperiod  46076  sumnnodd  46078  limcresiooub  46088  limcresioolb  46089  0ellimcdiv  46095  reclimc  46099  limsupval3  46138  limsupequzmpt2  46164  liminfval5  46211  limsupresxr  46212  liminfresxr  46213  liminfvalxr  46229  liminfequzmpt2  46237  climliminflimsupd  46247  liminfltlem  46250  liminflbuz2  46261  sinmulcos  46311  coskpi2  46312  cncfdmsn  46336  cncfiooicclem1  46339  fprodsubrecnncnvlem  46353  fprodaddrecnncnvlem  46355  fperdvper  46365  dvnmptdivc  46384  dvnxpaek  46388  dvnmul  46389  dvnprodlem1  46392  dvnprodlem3  46394  itgcoscmulx  46415  itgsincmulx  46420  itgspltprt  46425  itgiccshift  46426  itgperiod  46427  sublevolico  46430  volioof  46433  ovolsplit  46434  fvvolioof  46435  fvvolicof  46437  stoweidlem22  46468  stoweidlem32  46478  wallispilem5  46515  stirlinglem5  46524  dirkertrigeqlem2  46545  dirkertrigeq  46547  dirkercncflem1  46549  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem13  46566  fourierdlem16  46569  fourierdlem19  46572  fourierdlem21  46574  fourierdlem22  46575  fourierdlem28  46581  fourierdlem32  46585  fourierdlem33  46586  fourierdlem42  46595  fourierdlem47  46599  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem56  46608  fourierdlem60  46612  fourierdlem61  46613  fourierdlem64  46616  fourierdlem66  46618  fourierdlem71  46623  fourierdlem73  46625  fourierdlem74  46626  fourierdlem76  46628  fourierdlem78  46630  fourierdlem79  46631  fourierdlem80  46632  fourierdlem81  46633  fourierdlem83  46635  fourierdlem88  46640  fourierdlem92  46644  fourierdlem93  46645  fourierdlem97  46649  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem109  46661  fourierdlem111  46663  fouriersw  46677  elaa2lem  46679  etransclem24  46704  etransclem25  46705  etransclem35  46715  etransclem46  46726  rrndistlt  46736  rrxunitopnfi  46738  qndenserrnbl  46741  qndenserrnopnlem  46743  saldifcl2  46774  intsal  46776  sge0sn  46825  sge0ltfirp  46846  sge0iunmptlemre  46861  sge0fodjrnlem  46862  sge0isum  46873  sge0xaddlem1  46879  nnfoctbdjlem  46901  meassle  46909  ismeannd  46913  meadif  46925  meaiuninclem  46926  meaiininclem  46932  omeunile  46951  caragendifcl  46960  caratheodory  46974  isomenndlem  46976  ovnsubaddlem1  47016  hoidmv1lelem2  47038  hoidmv1le  47040  hoidmvlelem2  47042  hoidmvle  47046  hoi2toco  47053  rrnmbl  47060  hoidifhspdmvle  47066  voncmpl  47067  hoiqssbl  47071  hspmbllem1  47072  hspmbllem2  47073  ovolval2lem  47089  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  hoimbl2  47111  vonhoire  47118  salpreimagelt  47153  salpreimalegt  47155  preimaioomnf  47165  smfres  47236  smfmullem1  47237  smflimmpt  47256  smfsupmpt  47261  smfinfmpt  47265  smflimsupmpt  47275  smfliminflem  47276  smfliminfmpt  47278  sigarcol  47310  sin5tlem2  47338  f1oresf1o  47750  elsprel  47947  prproropf1o  47979  paireqne  47983  sfprmdvdsmersenne  48078  lighneallem3  48082  lighneallem4  48085  nprmdvdsfacm1lem1  48095  nn0onn0exALTV  48187  nnsum3primesprm  48278  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  isuspgrim0lem  48381  clnbgrgrimlem  48421  uspgrlimlem3  48478  uspgrlimlem4  48479  gpgedgvtx0  48549  gpgedgvtx1  48550  funcringcsetcALTV2lem7  48784  funcringcsetclem7ALTV  48807  lincext3  48944  lincresunit3  48969  nn0onn0ex  49011  nnpw2pmod  49071  blennn0em1  49079  digexp  49095  dignn0ehalf  49105  nn0mulfsum  49112  itcovalpclem1  49158  eenglngeehlnmlem2  49226  rrx2vlinest  49229  line2  49240  itschlc0xyqsol  49255  itsclinecirc0b  49262  toplatjoin  49489  toplatmeet  49490  upeu2lem  49515  oppff1o  49636  imaf1co  49642  upciclem3  49655  natoppfb  49718  oppcthinco  49926  oppcthinendcALT  49928  lmddu  50154  recsec  50243  reccsc  50244  aacllem  50288  amgmlemALT  50290