Theorem eqtr2d 2774

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 2773	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2739	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  3eqtrrd  2778  3eqtr2rd  2780  ifan  4581  ifor  4582  dfopif  4870  fnco  6665  fnsnfv  6968  nvocnv  7276  elovmpt3rab1  7663  onsucmin  7806  csbopeq1a  8033  oaabs2  8645  ecinxp  8783  fsetfocdm  8852  resixpfo  8927  sbthlem3  9082  rankxpsuc  9874  fseqenlem2  10017  dfac2b  10122  isf32lem9  10353  compsscnvlem  10362  ttukeylem7  10507  fpwwe2lem10  10632  00id  11386  submul2  11651  mulsubfacd  11672  divadddiv  11926  infrenegsup  12194  xadd4d  13279  fzdifsuc  13558  fzval3  13698  fzoshftral  13746  ceim1l  13809  fldiv  13822  flmod  13847  intfrac  13848  modcyc2  13869  moddi  13901  uzrdgfni  13920  axdc4uzlem  13945  seqf1olem1  14004  seqf1olem2  14005  seqid2  14011  expnegz  14059  binom2sub  14180  binom3  14184  hashreshashfun  14396  ccatw2s1p2  14584  ccats1pfxeq  14661  pfxccatin12lem2  14678  pfxccatin12  14680  swrdccat3b  14687  cshweqrep  14768  2cshwcshw  14773  ccatco  14783  swrds2  14888  relexpsucnnr  14969  relexpaddnn  14995  reim  15053  mulre  15065  addcj  15092  absimle  15253  clim2ser  15598  isercoll2  15612  serf0  15624  iseralt  15628  summolem3  15657  isumclim3  15702  mptfzshft  15721  fsumrev  15722  fsum2mul  15732  incexc  15780  isumsplit  15783  mertenslem1  15827  fprodrev  15918  iprodclim3  15941  binomfallfaclem2  15981  ef4p  16053  tanval3  16074  efival  16092  sinmul  16112  bitsinvp1  16387  sadaddlem  16404  bitsshft  16413  smu01lem  16423  dfgcd2  16485  lcmgcdlem  16540  lcm1  16544  lcmfass  16580  eulerthlem2  16712  hashgcdeq  16719  powm2modprm  16733  pythagtriplem16  16760  pczpre  16777  pcqdiv  16787  pcadd  16819  pcfac  16829  prmreclem5  16850  4sqlem10  16877  4sqlem19  16893  vdwapun  16904  vdwlem1  16911  ramcl  16959  setsstruct  17106  strfvd  17131  strfv2d  17132  xpsff1o  17510  xpsrnbas  17514  2oppccomf  17668  oppcepi  17683  sscfn1  17761  sscfn2  17762  invfuc  17924  funcestrcsetclem7  18095  funcsetcestrclem7  18110  gsumsplit1r  18603  grpinvssd  18897  grpinvval2  18903  cycsubggend  19077  pmtrdifwrdellem2  19345  psgnunilem1  19356  psgnuni  19362  pgp0  19459  sylow1lem1  19461  sylow3lem2  19491  efgredleme  19606  efgcpbllemb  19618  frgpuptinv  19634  frgpup3lem  19640  gexexlem  19715  cyggenod  19747  gsumval3eu  19767  gsumval3  19770  gsumzaddlem  19784  dprd2db  19908  ablsimpgfindlem1  19972  ringinvdv  20221  lss1d  20567  pwssplit1  20663  znzrh2  21093  regsumsupp  21167  ipassr2  21192  dsmmfi  21285  frlmlss  21298  frlmip  21325  frlmlbs  21344  frlmup3  21347  islindf4  21385  mplcoe3  21585  subrgascl  21619  evlseu  21638  ply1sclid  21802  1marepvmarrepid  22069  madurid  22138  smadiadetlem3  22162  mat2pmatghm  22224  pmatcollpwscmatlem1  22283  pm2mpmhmlem2  22313  cpmadurid  22361  cpmidgsumm2pm  22363  cpmadugsumlemB  22368  cayhamlem2  22378  ntrval2  22547  ordtuni  22686  cnclima  22764  cmpsub  22896  ptbasfi  23077  txbasval  23102  pt1hmeo  23302  alexsubALTlem1  23543  trust  23726  ussid  23757  ressuss  23759  ressprdsds  23869  imasdsf1olem  23871  setsms  23980  tmsxms  23987  tmsxpsmopn  24038  subgnm  24134  tngnm  24160  tngngp2  24161  xrsxmet  24317  xrge0gsumle  24341  metdstri  24359  xrhmeo  24454  lebnumlem3  24471  pcorevlem  24534  pi1xfrcnvlem  24564  clmabs  24591  cvsmuleqdivd  24642  rrxip  24899  rrxds  24902  rrxdsfi  24920  minveclem4a  24939  pjthlem1  24946  divcncf  24956  ovolunlem1a  25005  mbfres2  25154  i1faddlem  25202  ibladdlem  25329  iblabs  25338  ditgsplit  25370  dvmptresicc  25425  dvnres  25440  dvmptdiv  25483  dveflem  25488  dveq0  25509  dvfsumabs  25532  itgsubstlem  25557  ply1divex  25646  dgrco  25781  plycjlem  25782  taylthlem1  25877  pserdv2  25934  abelthlem6  25940  abelthlem7  25942  tangtx  26007  abssinper  26022  sineq0  26025  explog  26094  reexplog  26095  eflogeq  26102  abslogle  26118  tanarg  26119  logtayl  26160  logtayl2  26162  relogbdiv  26274  ang180lem3  26306  affineequiv  26318  affineequiv2  26319  chordthmlem4  26330  chordthmlem5  26331  heron  26333  dcubic1lem  26338  dcubic2  26339  dcubic  26341  mcubic  26342  cubic2  26343  dquartlem1  26346  dquart  26348  quart1lem  26350  quartlem1  26352  quart  26356  acoscos  26388  atanlogaddlem  26408  atantayl2  26433  atantayl3  26434  birthdaylem2  26447  efrlim  26464  amgmlem  26484  logdifbnd  26488  emcllem3  26492  emcllem6  26495  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  gamigam  26547  lgamcvg2  26549  gamfac  26561  basellem3  26577  basellem8  26582  basellem9  26583  chtprm  26647  logfaclbnd  26715  perfect1  26721  bcp1ctr  26772  bclbnd  26773  bposlem1  26777  lgsdilem  26817  lgsdirnn0  26837  lgsdinn0  26838  gausslemma2dlem1a  26858  gausslemma2dlem4  26862  gausslemma2dlem5a  26863  lgseisenlem2  26869  lgsquadlem1  26873  2sqlem2  26911  mul2sq  26912  2sqmod  26929  2sqnn0  26931  vmadivsum  26975  rpvmasumlem  26980  dchrisumlem1  26982  dchrisumlem2  26983  dchrmusum2  26987  dchrvmasum2if  26990  dchrisum0lem2  27011  logsqvma2  27036  selberg3  27052  selberg4lem1  27053  pntrsumo1  27058  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem5  27074  pntibndlem2  27084  pntlemk  27099  pntlemo  27100  ostth2lem4  27129  ostth3  27131  tgbtwndiff  27747  tgifscgr  27749  trgcgrg  27756  motcgr3  27786  tgbtwnconn1lem1  27813  tgbtwnconn1lem2  27814  ismir  27900  miriso  27911  midexlem  27933  ragmir  27941  footexALT  27959  footexlem1  27960  footexlem2  27961  colperpexlem3  27973  mideulem2  27975  midex  27978  opphllem3  27990  midcgr  28021  lmiisolem  28037  brbtwn2  28153  colinearalglem4  28157  axsegconlem1  28165  axpaschlem  28188  axcontlem4  28215  axcontlem7  28218  axcontlem8  28219  ushgredgedgloop  28478  crctcshwlkn0lem6  29059  wwlknlsw  29091  wwlksnextwrd  29141  clwlkclwwlklem2a3  29237  clwlkclwwlk2  29246  clwwlkel  29289  clwwlkfo  29293  clwwlkext2edg  29299  eupth2eucrct  29460  numclwwlk2lem1lem  29585  numclwwlk1lem2fo  29601  numclwlk2lem2f  29620  grpoidinvlem2  29746  nvmtri  29912  cnnvm  29923  nvnd  29929  ipidsq  29951  ipnm  29952  ipipcj  29956  blocnilem  30045  ipasslem2  30073  dipsubdir  30089  hvaddsubval  30274  pjhthlem1  30632  pjspansn  30818  pjo  30912  unoplin  31161  adjadj  31177  hmoplin  31183  eigvec1  31203  lnopeqi  31249  nmcexi  31267  lnfnsubi  31287  riesz3i  31303  kbass6  31362  leoprf2  31368  leoprf  31369  pjnmopi  31389  mdslmd1lem1  31566  mdslmd1lem2  31567  superpos  31595  ifeq3da  31766  fgreu  31885  resf1o  31943  fprodex01  32019  wrdt2ind  32105  gsummpt2d  32189  xrge0tsmseq  32199  symgfcoeu  32231  psgnfzto1stlem  32247  psgnfzto1st  32252  cycpm2tr  32266  cycpmco2lem6  32278  cycpmco2lem7  32279  subrgchr  32375  rhmdvd  32425  qusrn  32509  nsgqusf1olem3  32515  rhmquskerlem  32532  elrspunsn  32536  mxidlirredi  32576  qsdrngi  32598  evls1addd  32637  evls1muld  32638  evls1vsca  32639  ply1chr  32650  dimval  32675  dimvalfi  32676  lindsunlem  32698  dimkerim  32701  qusdimsum  32702  fedgmullem1  32703  extdg1id  32731  evls1maprhm  32748  evls1maplmhm  32749  evls1maprnss  32750  ply1annidllem  32751  algextdeglem1  32761  madjusmdetlem2  32797  qtophaus  32805  zarclssn  32842  zarcmplem  32850  pstmval  32864  mndpluscn  32895  qqhucn  32961  esumval  33033  gsumesum  33046  esumcst  33050  esumpcvgval  33065  oddpwdc  33342  eulerpartlemgvv  33364  probdif  33408  sgnmul  33530  signsvtn  33584  actfunsnf1o  33605  reprpmtf1o  33627  hgt750lemd  33649  logdivsqrle  33651  hgt750lemg  33655  hgt750lemb  33657  bnj1415  34038  swrdrevpfx  34096  pfxwlk  34103  derangen2  34154  subfaclefac  34156  subfaclim  34168  satom  34336  fmla  34361  mrsubrn  34493  sinccvglem  34646  bcprod  34697  filnetlem4  35255  curunc  36459  ltflcei  36465  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem24  36501  mblfinlem4  36517  ibladdnclem  36533  iblabsnc  36541  iblmulc2nc  36542  ftc1anclem6  36555  ftc1anclem8  36557  sdclem2  36599  ismtycnv  36659  heiborlem10  36677  lflvsass  37940  lkrscss  37957  eqlkr  37958  eqlkr3  37960  ldualvsdi2  38003  omllaw3  38104  cmtcomlemN  38107  cmtbr3N  38113  omlfh3N  38118  llnexchb2lem  38728  dalawlem7  38737  dalawlem11  38741  dalawlem12  38742  pol1N  38770  paddatclN  38809  4atexlemcnd  38932  ltrncoidN  38988  cdleme3b  39089  cdleme11  39130  cdleme15a  39134  cdleme22e  39204  cdleme22g  39208  cdlemg18b  39539  trlcoat  39583  cdlemk2  39692  cdlemk4  39694  cdlemki  39701  cdlemksv2  39707  cdlemk15  39715  cdlemk55a  39819  diainN  39917  dia2dimlem3  39926  dia2dimlem5  39928  dvhlveclem  39968  diaocN  39985  cdlemn4  40058  cdlemn8  40064  dihopelvalcpre  40108  dihmeetlem9N  40175  dih1dimatlem  40189  dihpN  40196  dochvalr3  40223  dochsat  40243  djhjlj  40263  dochdmm1  40270  dihjatcclem4  40281  dihjat1  40289  dihjat4  40293  dochsnkr2cl  40334  dochfl1  40336  lclkrlem2j  40376  mapdordlem2  40497  mapdrvallem2  40505  hdmap10  40700  lcmineqlem12  40894  3lexlogpow5ineq5  40914  aks4d1p1  40930  frlmvscadiccat  41078  grpcominv1  41080  riccrng1  41094  ricdrng1  41100  frlmsnic  41108  evlselv  41157  fsuppind  41160  nicomachus  41206  sumcubes  41207  cnreeu  41338  flt4lem7  41398  negexpidd  41406  3cubeslem2  41409  3cubeslem3r  41411  mzpsubmpt  41467  irrapxlem3  41548  pellexlem6  41558  pell1234qrne0  41577  pell1234qrreccl  41578  pell1234qrmulcl  41579  pell14qrdich  41593  pell1qrgaplem  41597  rmxluc  41661  rmyluc  41662  jm2.24nn  41684  jm2.18  41713  jm2.19lem2  41715  jm2.19lem3  41716  jm2.22  41720  jm2.23  41721  jm2.16nn0  41729  jm2.27c  41732  fnwe2lem2  41779  lmhmfgsplit  41814  hbtlem2  41852  onsucf1lem  42005  ofoafo  42092  naddcnffo  42100  naddwordnexlem4  42138  reabssgn  42373  relexpmulnn  42446  relexpmulg  42447  ntrclsneine0lem  42801  int-addassocd  42912  dvconstbi  43079  bccm1k  43087  binomcxplemnotnn0  43101  fmptsnxp  43851  wessf1ornlem  43868  projf1o  43882  infnsuprnmpt  43941  lefldiveq  43989  lt4addmuld  44003  fzdifsuc2  44007  suplesup  44036  infrpge  44048  xrlexaddrp  44049  xralrple2  44051  infleinflem1  44067  supminfrnmpt  44142  supminfxr2  44166  fsumnncl  44275  limcperiod  44331  sumnnodd  44333  limcresiooub  44345  limcresioolb  44346  0ellimcdiv  44352  reclimc  44356  limsupval3  44395  limsupequzmpt2  44421  liminfval5  44468  limsupresxr  44469  liminfresxr  44470  liminfvalxr  44486  liminfequzmpt2  44494  climliminflimsupd  44504  liminfltlem  44507  liminflbuz2  44518  sinmulcos  44568  coskpi2  44569  cncfdmsn  44593  cncfiooicclem1  44596  fprodsubrecnncnvlem  44610  fprodaddrecnncnvlem  44612  fperdvper  44622  dvnmptdivc  44641  dvnxpaek  44645  dvnmul  44646  dvnprodlem1  44649  dvnprodlem3  44651  itgcoscmulx  44672  itgsincmulx  44677  itgspltprt  44682  itgiccshift  44683  itgperiod  44684  sublevolico  44687  volioof  44690  ovolsplit  44691  fvvolioof  44692  fvvolicof  44694  stoweidlem22  44725  stoweidlem32  44735  wallispilem5  44772  stirlinglem5  44781  dirkertrigeqlem2  44802  dirkertrigeq  44804  dirkercncflem1  44806  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem13  44823  fourierdlem16  44826  fourierdlem19  44829  fourierdlem21  44831  fourierdlem22  44832  fourierdlem28  44838  fourierdlem32  44842  fourierdlem33  44843  fourierdlem42  44852  fourierdlem47  44856  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem56  44865  fourierdlem60  44869  fourierdlem61  44870  fourierdlem64  44873  fourierdlem66  44875  fourierdlem71  44880  fourierdlem73  44882  fourierdlem74  44883  fourierdlem76  44885  fourierdlem78  44887  fourierdlem79  44888  fourierdlem80  44889  fourierdlem81  44890  fourierdlem83  44892  fourierdlem88  44897  fourierdlem92  44901  fourierdlem93  44902  fourierdlem97  44906  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  fourierdlem109  44918  fourierdlem111  44920  fouriersw  44934  elaa2lem  44936  etransclem24  44961  etransclem25  44962  etransclem35  44972  etransclem46  44983  rrndistlt  44993  rrxunitopnfi  44995  qndenserrnbl  44998  qndenserrnopnlem  45000  saldifcl2  45031  intsal  45033  sge0sn  45082  sge0ltfirp  45103  sge0iunmptlemre  45118  sge0fodjrnlem  45119  sge0isum  45130  sge0xaddlem1  45136  nnfoctbdjlem  45158  meassle  45166  ismeannd  45170  meadif  45182  meaiuninclem  45183  meaiininclem  45189  omeunile  45208  caragendifcl  45217  caratheodory  45231  isomenndlem  45233  ovnsubaddlem1  45273  hoidmv1lelem2  45295  hoidmv1le  45297  hoidmvlelem2  45299  hoidmvle  45303  hoi2toco  45310  rrnmbl  45317  hoidifhspdmvle  45323  voncmpl  45324  hoiqssbl  45328  hspmbllem1  45329  hspmbllem2  45330  ovolval2lem  45346  ovolval5lem2  45356  ovnovollem1  45359  ovnovollem2  45360  hoimbl2  45368  vonhoire  45375  salpreimagelt  45410  salpreimalegt  45412  preimaioomnf  45422  smfres  45493  smfmullem1  45494  smflimmpt  45513  smfsupmpt  45518  smfinfmpt  45522  smflimsupmpt  45532  smfliminflem  45533  smfliminfmpt  45535  sigarcol  45567  f1oresf1o  45985  elsprel  46130  prproropf1o  46162  paireqne  46166  sfprmdvdsmersenne  46258  lighneallem3  46262  lighneallem4  46265  nn0onn0exALTV  46354  nnsum3primesprm  46445  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  c0snmgmhm  46699  rngqiprnglin  46768  rngcifuestrc  46849  funcrngcsetc  46850  funcrngcsetcALT  46851  funcringcsetc  46887  funcringcsetcALTV2lem7  46894  funcringcsetclem7ALTV  46917  lincext3  47091  lincresunit3  47116  nn0onn0ex  47163  nnpw2pmod  47223  blennn0em1  47231  digexp  47247  dignn0ehalf  47257  nn0mulfsum  47264  itcovalpclem1  47310  eenglngeehlnmlem2  47378  rrx2vlinest  47381  line2  47392  itschlc0xyqsol  47407  itsclinecirc0b  47414  toplatjoin  47581  toplatmeet  47582  recsec  47755  reccsc  47756  aacllem  47802  amgmlemALT  47804