Theorem eqtr2d 2778

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3eqtrrd  2782  3eqtr2rd  2784  ifan  4579  ifor  4580  dfopif  4870  fnco  6686  fnsnfv  6988  nvocnv  7301  elovmpt3rab1  7693  onsucmin  7841  csbopeq1a  8075  oaabs2  8687  ecinxp  8832  resixpfo  8976  sbthlem3  9125  rankxpsuc  9922  fseqenlem2  10065  dfac2b  10171  isf32lem9  10401  compsscnvlem  10410  ttukeylem7  10555  fpwwe2lem10  10680  00id  11436  submul2  11703  mulsubfacd  11724  divadddiv  11982  infrenegsup  12251  xadd4d  13345  fzdifsuc  13624  fzval3  13773  fzoshftral  13823  ceim1l  13887  fldiv  13900  flmod  13925  intfrac  13926  modcyc2  13947  moddi  13980  uzrdgfni  13999  axdc4uzlem  14024  seqf1olem1  14082  seqf1olem2  14083  seqid2  14089  expnegz  14137  binom2sub  14259  binom3  14263  hashreshashfun  14478  ccatw2s1p2  14675  ccats1pfxeq  14752  pfxccatin12lem2  14769  pfxccatin12  14771  swrdccat3b  14778  cshweqrep  14859  2cshwcshw  14864  ccatco  14874  swrds2  14979  relexpsucnnr  15064  relexpaddnn  15090  reim  15148  mulre  15160  addcj  15187  absimle  15348  clim2ser  15691  isercoll2  15705  serf0  15717  iseralt  15721  summolem3  15750  isumclim3  15795  mptfzshft  15814  fsumrev  15815  fsum2mul  15825  incexc  15873  isumsplit  15876  mertenslem1  15920  fprodrev  16013  iprodclim3  16036  binomfallfaclem2  16076  ef4p  16149  tanval3  16170  efival  16188  sinmul  16208  bitsinvp1  16486  sadaddlem  16503  bitsshft  16512  smu01lem  16522  dfgcd2  16583  lcmgcdlem  16643  lcm1  16647  lcmfass  16683  eulerthlem2  16819  hashgcdeq  16827  powm2modprm  16841  pythagtriplem16  16868  pczpre  16885  pcqdiv  16895  pcadd  16927  pcfac  16937  prmreclem5  16958  4sqlem10  16985  4sqlem19  17001  vdwapun  17012  vdwlem1  17019  ramcl  17067  setsstruct  17213  strfvd  17237  strfv2d  17238  xpsff1o  17612  xpsrnbas  17616  2oppccomf  17768  oppcepi  17783  sscfn1  17861  sscfn2  17862  invfuc  18022  funcestrcsetclem7  18191  funcsetcestrclem7  18206  gsumsplit1r  18700  grpinvssd  19035  grpinvval2  19041  cycsubggend  19223  pmtrdifwrdellem2  19500  psgnunilem1  19511  psgnuni  19517  pgp0  19614  sylow1lem1  19616  sylow3lem2  19646  efgredleme  19761  efgcpbllemb  19773  frgpuptinv  19789  frgpup3lem  19795  gexexlem  19870  cyggenod  19902  gsumval3eu  19922  gsumval3  19925  gsumzaddlem  19939  dprd2db  20063  ablsimpgfindlem1  20127  ringinvdv  20414  c0snmgmhm  20462  rngcifuestrc  20639  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  lss1d  20961  pwssplit1  21058  rhmqusnsg  21295  rngqiprnglin  21312  znzrh2  21564  regsumsupp  21640  ipassr2  21665  dsmmfi  21758  frlmlss  21771  frlmip  21798  frlmlbs  21817  frlmup3  21820  islindf4  21858  mplcoe3  22056  subrgascl  22090  evlseu  22107  psdadd  22167  ply1sclid  22291  ply1chr  22310  evls1addd  22375  evls1muld  22376  evls1vsca  22377  evls1maprhm  22380  evls1maplmhm  22381  evls1maprnss  22382  evl1maprhm  22383  1marepvmarrepid  22581  madurid  22650  smadiadetlem3  22674  mat2pmatghm  22736  pmatcollpwscmatlem1  22795  pm2mpmhmlem2  22825  cpmadurid  22873  cpmidgsumm2pm  22875  cpmadugsumlemB  22880  cayhamlem2  22890  ntrval2  23059  ordtuni  23198  cnclima  23276  cmpsub  23408  ptbasfi  23589  txbasval  23614  pt1hmeo  23814  alexsubALTlem1  24055  trust  24238  ussid  24269  ressuss  24271  ressprdsds  24381  imasdsf1olem  24383  setsms  24492  tmsxms  24499  tmsxpsmopn  24550  subgnm  24646  tngnm  24672  tngngp2  24673  xrsxmet  24831  xrge0gsumle  24855  metdstri  24873  xrhmeo  24977  lebnumlem3  24995  pcorevlem  25059  pi1xfrcnvlem  25089  clmabs  25116  cvsmuleqdivd  25167  rrxip  25424  rrxds  25427  rrxdsfi  25445  minveclem4a  25464  pjthlem1  25471  divcncf  25482  ovolunlem1a  25531  mbfres2  25680  i1faddlem  25728  ibladdlem  25855  iblabs  25864  ditgsplit  25896  dvmptresicc  25951  dvnres  25967  dvmptdiv  26012  dveflem  26017  dveq0  26039  dvfsumabs  26063  itgsubstlem  26089  ply1divex  26176  r1pid2  26201  dgrco  26315  plycjlem  26316  taylthlem1  26415  pserdv2  26474  abelthlem6  26480  abelthlem7  26482  tangtx  26547  abssinper  26563  sineq0  26566  explog  26636  reexplog  26637  eflogeq  26644  abslogle  26660  tanarg  26661  logtayl  26702  logtayl2  26704  relogbdiv  26822  ang180lem3  26854  affineequiv  26866  affineequiv2  26867  chordthmlem4  26878  chordthmlem5  26879  heron  26881  dcubic1lem  26886  dcubic2  26887  dcubic  26889  mcubic  26890  cubic2  26891  dquartlem1  26894  dquart  26896  quart1lem  26898  quartlem1  26900  quart  26904  acoscos  26936  atanlogaddlem  26956  atantayl2  26981  atantayl3  26982  birthdaylem2  26995  efrlim  27012  efrlimOLD  27013  amgmlem  27033  logdifbnd  27037  emcllem3  27041  emcllem6  27044  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  gamigam  27096  lgamcvg2  27098  gamfac  27110  basellem3  27126  basellem8  27131  basellem9  27132  chtprm  27196  logfaclbnd  27266  perfect1  27272  bcp1ctr  27323  bclbnd  27324  bposlem1  27328  lgsdilem  27368  lgsdirnn0  27388  lgsdinn0  27389  gausslemma2dlem1a  27409  gausslemma2dlem4  27413  gausslemma2dlem5a  27414  lgseisenlem2  27420  lgsquadlem1  27424  2sqlem2  27462  mul2sq  27463  2sqmod  27480  2sqnn0  27482  vmadivsum  27526  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasum2if  27541  dchrisum0lem2  27562  logsqvma2  27587  selberg3  27603  selberg4lem1  27604  pntrsumo1  27609  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem5  27625  pntibndlem2  27635  pntlemk  27650  pntlemo  27651  ostth2lem4  27680  ostth3  27682  subsfo  28095  negsval2  28096  sltonold  28283  noseqrdgfn  28312  addhalfcut  28419  tgbtwndiff  28514  tgifscgr  28516  trgcgrg  28523  motcgr3  28553  tgbtwnconn1lem1  28580  tgbtwnconn1lem2  28581  ismir  28667  miriso  28678  midexlem  28700  ragmir  28708  footexALT  28726  footexlem1  28727  footexlem2  28728  colperpexlem3  28740  mideulem2  28742  midex  28745  opphllem3  28757  midcgr  28788  lmiisolem  28804  brbtwn2  28920  colinearalglem4  28924  axsegconlem1  28932  axpaschlem  28955  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  ushgredgedgloop  29248  crctcshwlkn0lem6  29835  wwlknlsw  29867  wwlksnextwrd  29917  clwlkclwwlklem2a3  30013  clwlkclwwlk2  30022  clwwlkel  30065  clwwlkfo  30069  clwwlkext2edg  30075  eupth2eucrct  30236  numclwwlk2lem1lem  30361  numclwwlk1lem2fo  30377  numclwlk2lem2f  30396  grpoidinvlem2  30524  nvmtri  30690  cnnvm  30701  nvnd  30707  ipidsq  30729  ipnm  30730  ipipcj  30734  blocnilem  30823  ipasslem2  30851  dipsubdir  30867  hvaddsubval  31052  pjhthlem1  31410  pjspansn  31596  pjo  31690  unoplin  31939  adjadj  31955  hmoplin  31961  eigvec1  31981  lnopeqi  32027  nmcexi  32045  lnfnsubi  32065  riesz3i  32081  kbass6  32140  leoprf2  32146  leoprf  32147  pjnmopi  32167  mdslmd1lem1  32344  mdslmd1lem2  32345  superpos  32373  ifeq3da  32559  fgreu  32682  resf1o  32741  quad3d  32754  fprodex01  32827  ccatws1f1o  32936  wrdt2ind  32938  mndlactfo  33032  mndractfo  33034  gsummpt2d  33052  xrge0tsmseq  33067  gsumwrd2dccatlem  33069  gsumwrd2dccat  33070  symgfcoeu  33102  wrdpmtrlast  33113  psgnfzto1stlem  33120  psgnfzto1st  33125  cycpm2tr  33139  cycpmco2lem6  33151  cycpmco2lem7  33152  subrgchr  33241  elrgspnlem1  33246  elrgspnlem3  33248  elrgspnsubrunlem1  33251  rloccring  33274  rhmdvd  33348  qusrn  33437  nsgqusf1olem3  33443  rhmquskerlem  33453  elrspunsn  33457  mxidlirredi  33499  qsdrngi  33523  1arithidomlem1  33563  1arithidomlem2  33564  evls1subd  33597  r1pid2OLD  33629  resssra  33638  dimval  33651  dimvalfi  33652  lindsunlem  33675  dimkerim  33678  qusdimsum  33679  fedgmullem1  33680  extdg1id  33716  fldextrspunlsplem  33723  fldextrspunlsp  33724  fldextrspunlem1  33725  fldextrspundgdvds  33731  ply1annidllem  33744  algextdeglem4  33761  constrrtcc  33776  constrsslem  33782  madjusmdetlem2  33827  qtophaus  33835  zarclssn  33872  zarcmplem  33880  pstmval  33894  mndpluscn  33925  qqhucn  33993  esumval  34047  gsumesum  34060  esumcst  34064  esumpcvgval  34079  oddpwdc  34356  eulerpartlemgvv  34378  probdif  34422  sgnmul  34545  signsvtn  34599  actfunsnf1o  34619  reprpmtf1o  34641  hgt750lemd  34663  logdivsqrle  34665  hgt750lemg  34669  hgt750lemb  34671  bnj1415  35052  swrdrevpfx  35122  pfxwlk  35129  derangen2  35179  subfaclefac  35181  subfaclim  35193  satom  35361  fmla  35386  mrsubrn  35518  sinccvglem  35677  bcprod  35738  filnetlem4  36382  curunc  37609  ltflcei  37615  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  mblfinlem4  37667  ibladdnclem  37683  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem6  37705  ftc1anclem8  37707  sdclem2  37749  ismtycnv  37809  heiborlem10  37827  lflvsass  39082  lkrscss  39099  eqlkr  39100  eqlkr3  39102  ldualvsdi2  39145  omllaw3  39246  cmtcomlemN  39249  cmtbr3N  39255  omlfh3N  39260  llnexchb2lem  39870  dalawlem7  39879  dalawlem11  39883  dalawlem12  39884  pol1N  39912  paddatclN  39951  4atexlemcnd  40074  ltrncoidN  40130  cdleme3b  40231  cdleme11  40272  cdleme15a  40276  cdleme22e  40346  cdleme22g  40350  cdlemg18b  40681  trlcoat  40725  cdlemk2  40834  cdlemk4  40836  cdlemki  40843  cdlemksv2  40849  cdlemk15  40857  cdlemk55a  40961  diainN  41059  dia2dimlem3  41068  dia2dimlem5  41070  dvhlveclem  41110  diaocN  41127  cdlemn4  41200  cdlemn8  41206  dihopelvalcpre  41250  dihmeetlem9N  41317  dih1dimatlem  41331  dihpN  41338  dochvalr3  41365  dochsat  41385  djhjlj  41405  dochdmm1  41412  dihjatcclem4  41423  dihjat1  41431  dihjat4  41435  dochsnkr2cl  41476  dochfl1  41478  lclkrlem2j  41518  mapdordlem2  41639  mapdrvallem2  41647  hdmap10  41842  lcmineqlem12  42041  3lexlogpow5ineq5  42061  aks4d1p1  42077  primrootsunit1  42098  primrootscoprmpow  42100  posbezout  42101  aks6d1c1p3  42111  aks6d1c1p4  42112  aks6d1c1p5  42113  aks6d1c1p7  42114  evl1gprodd  42118  hashscontpow1  42122  aks6d1c3  42124  aks6d1c2lem3  42127  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5lem3  42138  aks6d1c6lem1  42171  aks6d1c6isolem3  42177  aks6d1c6lem5  42178  bcle2d  42180  aks6d1c7lem1  42181  aks5lem3a  42190  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem4  42199  unitscyglem5  42200  aks5lem7  42201  nicomachus  42346  sumcubes  42347  cnreeu  42500  frlmvscadiccat  42516  grpcominv1  42518  riccrng1  42531  ricdrng1  42538  frlmsnic  42550  evlselv  42597  fsuppind  42600  flt4lem7  42669  negexpidd  42693  3cubeslem2  42696  3cubeslem3r  42698  mzpsubmpt  42754  irrapxlem3  42835  pellexlem6  42845  pell1234qrne0  42864  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell14qrdich  42880  pell1qrgaplem  42884  rmxluc  42948  rmyluc  42949  jm2.24nn  42971  jm2.18  43000  jm2.19lem2  43002  jm2.19lem3  43003  jm2.22  43007  jm2.23  43008  jm2.16nn0  43016  jm2.27c  43019  fnwe2lem2  43063  lmhmfgsplit  43098  hbtlem2  43136  onsucf1lem  43282  ofoafo  43369  naddcnffo  43377  naddwordnexlem4  43414  reabssgn  43649  relexpmulnn  43722  relexpmulg  43723  ntrclsneine0lem  44077  int-addassocd  44187  dvconstbi  44353  bccm1k  44361  binomcxplemnotnn0  44375  fmptsnxp  45174  wessf1ornlem  45190  projf1o  45202  infnsuprnmpt  45257  lefldiveq  45304  lt4addmuld  45318  fzdifsuc2  45322  suplesup  45350  infrpge  45362  xrlexaddrp  45363  xralrple2  45365  infleinflem1  45381  supminfrnmpt  45456  supminfxr2  45480  fsumnncl  45587  limcperiod  45643  sumnnodd  45645  limcresiooub  45657  limcresioolb  45658  0ellimcdiv  45664  reclimc  45668  limsupval3  45707  limsupequzmpt2  45733  liminfval5  45780  limsupresxr  45781  liminfresxr  45782  liminfvalxr  45798  liminfequzmpt2  45806  climliminflimsupd  45816  liminfltlem  45819  liminflbuz2  45830  sinmulcos  45880  coskpi2  45881  cncfdmsn  45905  cncfiooicclem1  45908  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  fperdvper  45934  dvnmptdivc  45953  dvnxpaek  45957  dvnmul  45958  dvnprodlem1  45961  dvnprodlem3  45963  itgcoscmulx  45984  itgsincmulx  45989  itgspltprt  45994  itgiccshift  45995  itgperiod  45996  sublevolico  45999  volioof  46002  ovolsplit  46003  fvvolioof  46004  fvvolicof  46006  stoweidlem22  46037  stoweidlem32  46047  wallispilem5  46084  stirlinglem5  46093  dirkertrigeqlem2  46114  dirkertrigeq  46116  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem13  46135  fourierdlem16  46138  fourierdlem19  46141  fourierdlem21  46143  fourierdlem22  46144  fourierdlem28  46150  fourierdlem32  46154  fourierdlem33  46155  fourierdlem42  46164  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem56  46177  fourierdlem60  46181  fourierdlem61  46182  fourierdlem64  46185  fourierdlem66  46187  fourierdlem71  46192  fourierdlem73  46194  fourierdlem74  46195  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem80  46201  fourierdlem81  46202  fourierdlem83  46204  fourierdlem88  46209  fourierdlem92  46213  fourierdlem93  46214  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem109  46230  fourierdlem111  46232  fouriersw  46246  elaa2lem  46248  etransclem24  46273  etransclem25  46274  etransclem35  46284  etransclem46  46295  rrndistlt  46305  rrxunitopnfi  46307  qndenserrnbl  46310  qndenserrnopnlem  46312  saldifcl2  46343  intsal  46345  sge0sn  46394  sge0ltfirp  46415  sge0iunmptlemre  46430  sge0fodjrnlem  46431  sge0isum  46442  sge0xaddlem1  46448  nnfoctbdjlem  46470  meassle  46478  ismeannd  46482  meadif  46494  meaiuninclem  46495  meaiininclem  46501  omeunile  46520  caragendifcl  46529  caratheodory  46543  isomenndlem  46545  ovnsubaddlem1  46585  hoidmv1lelem2  46607  hoidmv1le  46609  hoidmvlelem2  46611  hoidmvle  46615  hoi2toco  46622  rrnmbl  46629  hoidifhspdmvle  46635  voncmpl  46636  hoiqssbl  46640  hspmbllem1  46641  hspmbllem2  46642  ovolval2lem  46658  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  hoimbl2  46680  vonhoire  46687  salpreimagelt  46722  salpreimalegt  46724  preimaioomnf  46734  smfres  46805  smfmullem1  46806  smflimmpt  46825  smfsupmpt  46830  smfinfmpt  46834  smflimsupmpt  46844  smfliminflem  46845  smfliminfmpt  46847  sigarcol  46879  f1oresf1o  47302  elsprel  47462  prproropf1o  47494  paireqne  47498  sfprmdvdsmersenne  47590  lighneallem3  47594  lighneallem4  47597  nn0onn0exALTV  47686  nnsum3primesprm  47777  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  isuspgrim0lem  47871  clnbgrgrimlem  47901  uspgrlimlem3  47957  uspgrlimlem4  47958  gpgedgvtx0  48019  gpgedgvtx1  48020  funcringcsetcALTV2lem7  48212  funcringcsetclem7ALTV  48235  lincext3  48373  lincresunit3  48398  nn0onn0ex  48444  nnpw2pmod  48504  blennn0em1  48512  digexp  48528  dignn0ehalf  48538  nn0mulfsum  48545  itcovalpclem1  48591  eenglngeehlnmlem2  48659  rrx2vlinest  48662  line2  48673  itschlc0xyqsol  48688  itsclinecirc0b  48695  toplatjoin  48891  toplatmeet  48892  upeu2lem  48911  upciclem3  48925  oppcthinco  49088  oppcthinendcALT  49090  recsec  49275  reccsc  49276  aacllem  49320  amgmlemALT  49322