Theorem eqtr2d 2765

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 2764	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2735	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3eqtrrd  2769  3eqtr2rd  2771  ifan  4542  ifor  4543  dfopif  4834  fnco  6636  fnsnfv  6940  nvocnv  7256  elovmpt3rab1  7649  onsucmin  7796  csbopeq1a  8029  oaabs2  8613  ecinxp  8765  resixpfo  8909  sbthlem3  9053  rankxpsuc  9835  fseqenlem2  9978  dfac2b  10084  isf32lem9  10314  compsscnvlem  10323  ttukeylem7  10468  fpwwe2lem10  10593  00id  11349  submul2  11618  mulsubfacd  11639  divadddiv  11897  infrenegsup  12166  xadd4d  13263  fzdifsuc  13545  fzval3  13695  fzoshftral  13745  ceim1l  13809  fldiv  13822  flmod  13847  intfrac  13848  modcyc2  13869  modaddb  13871  moddi  13904  uzrdgfni  13923  axdc4uzlem  13948  seqf1olem1  14006  seqf1olem2  14007  seqid2  14013  expnegz  14061  binom2sub  14185  binom3  14189  hashreshashfun  14404  ccatw2s1p2  14602  ccats1pfxeq  14679  pfxccatin12lem2  14696  pfxccatin12  14698  swrdccat3b  14705  cshweqrep  14786  2cshwcshw  14791  ccatco  14801  swrds2  14906  relexpsucnnr  14991  relexpaddnn  15017  reim  15075  mulre  15087  addcj  15114  absimle  15275  clim2ser  15621  isercoll2  15635  serf0  15647  iseralt  15651  summolem3  15680  isumclim3  15725  mptfzshft  15744  fsumrev  15745  fsum2mul  15755  incexc  15803  isumsplit  15806  mertenslem1  15850  fprodrev  15943  iprodclim3  15966  binomfallfaclem2  16006  ef4p  16081  tanval3  16102  efival  16120  sinmul  16140  bitsinvp1  16419  sadaddlem  16436  bitsshft  16445  smu01lem  16455  dfgcd2  16516  lcmgcdlem  16576  lcm1  16580  lcmfass  16616  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  17530  xpsrnbas  17534  2oppccomf  17686  oppcepi  17701  sscfn1  17779  sscfn2  17780  invfuc  17939  funcestrcsetclem7  18107  funcsetcestrclem7  18122  gsumsplit1r  18614  grpinvssd  18949  grpinvval2  18955  cycsubggend  19137  pmtrdifwrdellem2  19412  psgnunilem1  19423  psgnuni  19429  pgp0  19526  sylow1lem1  19528  sylow3lem2  19558  efgredleme  19673  efgcpbllemb  19685  frgpuptinv  19701  frgpup3lem  19707  gexexlem  19782  cyggenod  19814  gsumval3eu  19834  gsumval3  19837  gsumzaddlem  19851  dprd2db  19975  ablsimpgfindlem1  20039  ringinvdv  20323  c0snmgmhm  20371  rngcifuestrc  20548  funcrngcsetc  20549  funcrngcsetcALT  20550  funcringcsetc  20583  lss1d  20869  pwssplit1  20966  rhmqusnsg  21195  rngqiprnglin  21212  znzrh2  21455  regsumsupp  21531  ipassr2  21556  dsmmfi  21647  frlmlss  21660  frlmip  21687  frlmlbs  21706  frlmup3  21709  islindf4  21747  mplcoe3  21945  subrgascl  21973  evlseu  21990  psdadd  22050  ply1sclid  22174  ply1chr  22193  evls1addd  22258  evls1muld  22259  evls1vsca  22260  evls1maprhm  22263  evls1maplmhm  22264  evls1maprnss  22265  evl1maprhm  22266  1marepvmarrepid  22462  madurid  22531  smadiadetlem3  22555  mat2pmatghm  22617  pmatcollpwscmatlem1  22676  pm2mpmhmlem2  22706  cpmadurid  22754  cpmidgsumm2pm  22756  cpmadugsumlemB  22761  cayhamlem2  22771  ntrval2  22938  ordtuni  23077  cnclima  23155  cmpsub  23287  ptbasfi  23468  txbasval  23493  pt1hmeo  23693  alexsubALTlem1  23934  trust  24117  ussid  24148  ressuss  24150  ressprdsds  24259  imasdsf1olem  24261  setsms  24368  tmsxms  24374  tmsxpsmopn  24425  subgnm  24521  tngnm  24539  tngngp2  24540  xrsxmet  24698  xrge0gsumle  24722  metdstri  24740  xrhmeo  24844  lebnumlem3  24862  pcorevlem  24926  pi1xfrcnvlem  24956  clmabs  24983  cvsmuleqdivd  25034  rrxip  25290  rrxds  25293  rrxdsfi  25311  minveclem4a  25330  pjthlem1  25337  divcncf  25348  ovolunlem1a  25397  mbfres2  25546  i1faddlem  25594  ibladdlem  25721  iblabs  25730  ditgsplit  25762  dvmptresicc  25817  dvnres  25833  dvmptdiv  25878  dveflem  25883  dveq0  25905  dvfsumabs  25929  itgsubstlem  25955  ply1divex  26042  r1pid2  26067  dgrco  26181  plycjlem  26182  taylthlem1  26281  pserdv2  26340  abelthlem6  26346  abelthlem7  26348  tangtx  26414  abssinper  26430  sineq0  26433  explog  26503  reexplog  26504  eflogeq  26511  abslogle  26527  tanarg  26528  logtayl  26569  logtayl2  26571  relogbdiv  26689  ang180lem3  26721  affineequiv  26733  affineequiv2  26734  chordthmlem4  26745  chordthmlem5  26746  heron  26748  dcubic1lem  26753  dcubic2  26754  dcubic  26756  mcubic  26757  cubic2  26758  dquartlem1  26761  dquart  26763  quart1lem  26765  quartlem1  26767  quart  26771  acoscos  26803  atanlogaddlem  26823  atantayl2  26848  atantayl3  26849  birthdaylem2  26862  efrlim  26879  efrlimOLD  26880  amgmlem  26900  logdifbnd  26904  emcllem3  26908  emcllem6  26911  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  gamigam  26963  lgamcvg2  26965  gamfac  26977  basellem3  26993  basellem8  26998  basellem9  26999  chtprm  27063  logfaclbnd  27133  perfect1  27139  bcp1ctr  27190  bclbnd  27191  bposlem1  27195  lgsdilem  27235  lgsdirnn0  27255  lgsdinn0  27256  gausslemma2dlem1a  27276  gausslemma2dlem4  27280  gausslemma2dlem5a  27281  lgseisenlem2  27287  lgsquadlem1  27291  2sqlem2  27329  mul2sq  27330  2sqmod  27347  2sqnn0  27349  vmadivsum  27393  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrmusum2  27405  dchrvmasum2if  27408  dchrisum0lem2  27429  logsqvma2  27454  selberg3  27470  selberg4lem1  27471  pntrsumo1  27476  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntibndlem2  27502  pntlemk  27517  pntlemo  27518  ostth2lem4  27547  ostth3  27549  subsfo  27969  negsval2  27970  sltonold  28162  noseqrdgfn  28200  n0sfincut  28246  addhalfcut  28334  tgbtwndiff  28433  tgifscgr  28435  trgcgrg  28442  motcgr3  28472  tgbtwnconn1lem1  28499  tgbtwnconn1lem2  28500  ismir  28586  miriso  28597  midexlem  28619  ragmir  28627  footexALT  28645  footexlem1  28646  footexlem2  28647  colperpexlem3  28659  mideulem2  28661  midex  28664  opphllem3  28676  midcgr  28707  lmiisolem  28723  brbtwn2  28832  colinearalglem4  28836  axsegconlem1  28844  axpaschlem  28867  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  ushgredgedgloop  29158  crctcshwlkn0lem6  29745  wwlknlsw  29777  wwlksnextwrd  29827  clwlkclwwlklem2a3  29923  clwlkclwwlk2  29932  clwwlkel  29975  clwwlkfo  29979  clwwlkext2edg  29985  eupth2eucrct  30146  numclwwlk2lem1lem  30271  numclwwlk1lem2fo  30287  numclwlk2lem2f  30306  grpoidinvlem2  30434  nvmtri  30600  cnnvm  30611  nvnd  30617  ipidsq  30639  ipnm  30640  ipipcj  30644  blocnilem  30733  ipasslem2  30761  dipsubdir  30777  hvaddsubval  30962  pjhthlem1  31320  pjspansn  31506  pjo  31600  unoplin  31849  adjadj  31865  hmoplin  31871  eigvec1  31891  lnopeqi  31937  nmcexi  31955  lnfnsubi  31975  riesz3i  31991  kbass6  32050  leoprf2  32056  leoprf  32057  pjnmopi  32077  mdslmd1lem1  32254  mdslmd1lem2  32255  superpos  32283  ifeq3da  32475  fgreu  32596  resf1o  32653  quad3d  32673  fprodex01  32750  sgnmul  32760  ccatws1f1o  32873  wrdt2ind  32875  mndlactfo  32968  mndractfo  32970  gsummpt2d  32989  xrge0tsmseq  33004  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  symgfcoeu  33039  wrdpmtrlast  33050  psgnfzto1stlem  33057  psgnfzto1st  33062  cycpm2tr  33076  cycpmco2lem6  33088  cycpmco2lem7  33089  subrgchr  33188  elrgspnlem1  33193  elrgspnlem3  33195  elrgspnsubrunlem1  33198  rloccring  33221  rhmdvd  33296  qusrn  33380  nsgqusf1olem3  33386  rhmquskerlem  33396  elrspunsn  33400  mxidlirredi  33442  qsdrngi  33466  1arithidomlem1  33506  1arithidomlem2  33507  evls1subd  33541  r1pid2OLD  33574  resssra  33583  dimval  33596  dimvalfi  33597  lindsunlem  33620  dimkerim  33623  qusdimsum  33624  fedgmullem1  33625  extdg1id  33661  fldextrspunlsplem  33668  fldextrspunlsp  33669  fldextrspunlem1  33670  fldextrspundgdvds  33676  ply1annidllem  33691  algextdeglem4  33710  constrrtcc  33725  constrsslem  33731  constrresqrtcl  33767  cos9thpiminplylem2  33773  cos9thpiminply  33778  madjusmdetlem2  33818  qtophaus  33826  zarclssn  33863  zarcmplem  33871  pstmval  33885  mndpluscn  33916  qqhucn  33982  esumval  34036  gsumesum  34049  esumcst  34053  esumpcvgval  34068  oddpwdc  34345  eulerpartlemgvv  34367  probdif  34411  signsvtn  34575  actfunsnf1o  34595  reprpmtf1o  34617  hgt750lemd  34639  logdivsqrle  34641  hgt750lemg  34645  hgt750lemb  34647  bnj1415  35028  swrdrevpfx  35104  pfxwlk  35111  derangen2  35161  subfaclefac  35163  subfaclim  35175  satom  35343  fmla  35368  mrsubrn  35500  sinccvglem  35659  bcprod  35725  filnetlem4  36369  curunc  37596  ltflcei  37602  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  mblfinlem4  37654  ibladdnclem  37670  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem6  37692  ftc1anclem8  37694  sdclem2  37736  ismtycnv  37796  heiborlem10  37814  lflvsass  39074  lkrscss  39091  eqlkr  39092  eqlkr3  39094  ldualvsdi2  39137  omllaw3  39238  cmtcomlemN  39241  cmtbr3N  39247  omlfh3N  39252  llnexchb2lem  39862  dalawlem7  39871  dalawlem11  39875  dalawlem12  39876  pol1N  39904  paddatclN  39943  4atexlemcnd  40066  ltrncoidN  40122  cdleme3b  40223  cdleme11  40264  cdleme15a  40268  cdleme22e  40338  cdleme22g  40342  cdlemg18b  40673  trlcoat  40717  cdlemk2  40826  cdlemk4  40828  cdlemki  40835  cdlemksv2  40841  cdlemk15  40849  cdlemk55a  40953  diainN  41051  dia2dimlem3  41060  dia2dimlem5  41062  dvhlveclem  41102  diaocN  41119  cdlemn4  41192  cdlemn8  41198  dihopelvalcpre  41242  dihmeetlem9N  41309  dih1dimatlem  41323  dihpN  41330  dochvalr3  41357  dochsat  41377  djhjlj  41397  dochdmm1  41404  dihjatcclem4  41415  dihjat1  41423  dihjat4  41427  dochsnkr2cl  41468  dochfl1  41470  lclkrlem2j  41510  mapdordlem2  41631  mapdrvallem2  41639  hdmap10  41834  lcmineqlem12  42028  3lexlogpow5ineq5  42048  aks4d1p1  42064  primrootsunit1  42085  primrootscoprmpow  42087  posbezout  42088  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1p7  42101  evl1gprodd  42105  hashscontpow1  42109  aks6d1c3  42111  aks6d1c2lem3  42114  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem3  42125  aks6d1c6lem1  42158  aks6d1c6isolem3  42164  aks6d1c6lem5  42165  bcle2d  42167  aks6d1c7lem1  42168  aks5lem3a  42177  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  aks5lem7  42188  nicomachus  42300  sumcubes  42301  cnreeu  42478  frlmvscadiccat  42494  grpcominv1  42496  riccrng1  42509  ricdrng1  42516  frlmsnic  42528  evlselv  42575  fsuppind  42578  flt4lem7  42647  negexpidd  42670  3cubeslem2  42673  3cubeslem3r  42675  mzpsubmpt  42731  irrapxlem3  42812  pellexlem6  42822  pell1234qrne0  42841  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell14qrdich  42857  pell1qrgaplem  42861  rmxluc  42925  rmyluc  42926  jm2.24nn  42948  jm2.18  42977  jm2.19lem2  42979  jm2.19lem3  42980  jm2.22  42984  jm2.23  42985  jm2.16nn0  42993  jm2.27c  42996  fnwe2lem2  43040  lmhmfgsplit  43075  hbtlem2  43113  onsucf1lem  43258  ofoafo  43345  naddcnffo  43353  naddwordnexlem4  43390  reabssgn  43625  relexpmulnn  43698  relexpmulg  43699  ntrclsneine0lem  44053  int-addassocd  44163  dvconstbi  44323  bccm1k  44331  binomcxplemnotnn0  44345  fmptsnxp  45163  wessf1ornlem  45179  projf1o  45191  infnsuprnmpt  45244  lefldiveq  45290  lt4addmuld  45304  fzdifsuc2  45308  suplesup  45335  infrpge  45347  xrlexaddrp  45348  xralrple2  45350  infleinflem1  45366  supminfrnmpt  45441  supminfxr2  45465  fsumnncl  45570  limcperiod  45626  sumnnodd  45628  limcresiooub  45640  limcresioolb  45641  0ellimcdiv  45647  reclimc  45651  limsupval3  45690  limsupequzmpt2  45716  liminfval5  45763  limsupresxr  45764  liminfresxr  45765  liminfvalxr  45781  liminfequzmpt2  45789  climliminflimsupd  45799  liminfltlem  45802  liminflbuz2  45813  sinmulcos  45863  coskpi2  45864  cncfdmsn  45888  cncfiooicclem1  45891  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  fperdvper  45917  dvnmptdivc  45936  dvnxpaek  45940  dvnmul  45941  dvnprodlem1  45944  dvnprodlem3  45946  itgcoscmulx  45967  itgsincmulx  45972  itgspltprt  45977  itgiccshift  45978  itgperiod  45979  sublevolico  45982  volioof  45985  ovolsplit  45986  fvvolioof  45987  fvvolicof  45989  stoweidlem22  46020  stoweidlem32  46030  wallispilem5  46067  stirlinglem5  46076  dirkertrigeqlem2  46097  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem13  46118  fourierdlem16  46121  fourierdlem19  46124  fourierdlem21  46126  fourierdlem22  46127  fourierdlem28  46133  fourierdlem32  46137  fourierdlem33  46138  fourierdlem42  46147  fourierdlem47  46151  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem56  46160  fourierdlem60  46164  fourierdlem61  46165  fourierdlem64  46168  fourierdlem66  46170  fourierdlem71  46175  fourierdlem73  46177  fourierdlem74  46178  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem80  46184  fourierdlem81  46185  fourierdlem83  46187  fourierdlem88  46192  fourierdlem92  46196  fourierdlem93  46197  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem109  46213  fourierdlem111  46215  fouriersw  46229  elaa2lem  46231  etransclem24  46256  etransclem25  46257  etransclem35  46267  etransclem46  46278  rrndistlt  46288  rrxunitopnfi  46290  qndenserrnbl  46293  qndenserrnopnlem  46295  saldifcl2  46326  intsal  46328  sge0sn  46377  sge0ltfirp  46398  sge0iunmptlemre  46413  sge0fodjrnlem  46414  sge0isum  46425  sge0xaddlem1  46431  nnfoctbdjlem  46453  meassle  46461  ismeannd  46465  meadif  46477  meaiuninclem  46478  meaiininclem  46484  omeunile  46503  caragendifcl  46512  caratheodory  46526  isomenndlem  46528  ovnsubaddlem1  46568  hoidmv1lelem2  46590  hoidmv1le  46592  hoidmvlelem2  46594  hoidmvle  46598  hoi2toco  46605  rrnmbl  46612  hoidifhspdmvle  46618  voncmpl  46619  hoiqssbl  46623  hspmbllem1  46624  hspmbllem2  46625  ovolval2lem  46641  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  hoimbl2  46663  vonhoire  46670  salpreimagelt  46705  salpreimalegt  46707  preimaioomnf  46717  smfres  46788  smfmullem1  46789  smflimmpt  46808  smfsupmpt  46813  smfinfmpt  46817  smflimsupmpt  46827  smfliminflem  46828  smfliminfmpt  46830  sigarcol  46862  f1oresf1o  47291  elsprel  47476  prproropf1o  47508  paireqne  47512  sfprmdvdsmersenne  47604  lighneallem3  47608  lighneallem4  47611  nn0onn0exALTV  47700  nnsum3primesprm  47791  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  isuspgrim0lem  47893  clnbgrgrimlem  47933  uspgrlimlem3  47989  uspgrlimlem4  47990  gpgedgvtx0  48052  gpgedgvtx1  48053  funcringcsetcALTV2lem7  48284  funcringcsetclem7ALTV  48307  lincext3  48445  lincresunit3  48470  nn0onn0ex  48512  nnpw2pmod  48572  blennn0em1  48580  digexp  48596  dignn0ehalf  48606  nn0mulfsum  48613  itcovalpclem1  48659  eenglngeehlnmlem2  48727  rrx2vlinest  48730  line2  48741  itschlc0xyqsol  48756  itsclinecirc0b  48763  toplatjoin  48990  toplatmeet  48991  upeu2lem  49017  oppff1o  49138  imaf1co  49144  upciclem3  49157  natoppfb  49220  oppcthinco  49428  oppcthinendcALT  49430  lmddu  49656  recsec  49745  reccsc  49746  aacllem  49790  amgmlemALT  49792