Theorem eqtr2d 2645

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  3eqtrrd  2649  3eqtr2rd  2651  ifan  4084  ifor  4085  dfopif  4337  nvocnv  6437  elovmpt3rab1  6791  onsucmin  6913  csbopeq1a  7112  oaabs2  7612  ecinxp  7709  resixpfo  7832  sbthlem3  7957  rankxpsuc  8628  fseqenlem2  8731  dfac2  8836  isf32lem9  9066  compsscnvlem  9075  ttukeylem7  9220  fpwwe2lem11  9341  00id  10090  submul2  10349  mulsubfacd  10371  divadddiv  10619  infrenegsup  10883  xadd4d  12005  fzdifsuc  12270  fzval3  12404  fzoshftral  12447  ceim1l  12508  fldiv  12521  flmod  12546  intfrac  12547  modcyc2  12568  moddi  12600  uzrdgfni  12619  axdc4uzlem  12644  seqf1olem1  12702  seqf1olem2  12703  seqid2  12709  expnegz  12756  binom2sub  12843  binom3  12847  wrdlenccats1lenm1  13252  ccatw2s1p2  13266  ccats1swrdeq  13321  swrdccatin12lem2  13340  swrdccatin12  13342  swrdccat3b  13347  cshweqrep  13418  2cshwcshw  13422  ccatco  13432  swrds2  13533  relexpsucnnr  13613  relexpaddnn  13639  reim  13697  mulre  13709  addcj  13736  absimle  13897  clim2ser  14233  isercoll2  14247  serf0  14259  iseralt  14263  summolem3  14292  isumclim3  14332  mptfzshft  14352  fsumrev  14353  fsum2mul  14363  incexc  14408  isumsplit  14411  mertenslem1  14455  fprodrev  14546  iprodclim3  14570  binomfallfaclem2  14610  ef4p  14682  tanval3  14703  efival  14721  sinmul  14741  bitsinvp1  15009  sadaddlem  15026  bitsshft  15035  smu01lem  15045  dfgcd2  15101  lcmgcdlem  15157  lcm1  15161  lcmfass  15197  eulerthlem2  15325  hashgcdeq  15332  powm2modprm  15346  pythagtriplem16  15373  pczpre  15390  pcqdiv  15400  pcadd  15431  pcfac  15441  prmreclem5  15462  4sqlem10  15489  4sqlem19  15505  vdwapun  15516  vdwlem1  15523  ramcl  15571  strfvd  15732  strfv2d  15733  xpsff1o  16051  xpslem  16056  2oppccomf  16208  oppcepi  16222  sscfn1  16300  sscfn2  16301  invfuc  16457  funcestrcsetclem7  16609  funcsetcestrclem7  16624  grpinvssd  17315  grpinvval2  17321  pmtrdifwrdellem2  17725  psgnunilem1  17736  psgnuni  17742  pgp0  17834  sylow1lem1  17836  sylow3lem2  17866  efgredleme  17979  efgcpbllemb  17991  frgpuptinv  18007  frgpup3lem  18013  gexexlem  18078  cyggenod  18109  gsumval3eu  18128  gsumval3  18131  gsumzaddlem  18144  dprd2db  18265  ringinvdv  18517  lss1d  18784  pwssplit1  18880  mplcoe3  19287  subrgascl  19319  evlseu  19337  ply1sclid  19479  znzrh2  19713  regsumsupp  19787  ipassr2  19811  dsmmfi  19901  frlmlss  19914  frlmip  19936  frlmlbs  19955  frlmup3  19958  islindf4  19996  1marepvmarrepid  20200  madurid  20269  smadiadetlem3  20293  mat2pmatghm  20354  pmatcollpwscmatlem1  20413  pm2mpmhmlem2  20443  cpmadurid  20491  cpmidgsumm2pm  20493  cpmadugsumlemB  20498  cayhamlem2  20508  ntrval2  20665  ordtuni  20804  cnclima  20882  cmpsub  21013  ptbasfi  21194  txbasval  21219  pt1hmeo  21419  alexsubALTlem1  21661  trust  21843  ussid  21874  ressuss  21877  ressprdsds  21986  imasdsf1olem  21988  setsms  22095  tmsxms  22101  tmsxpsmopn  22152  subgnm  22247  tngnm  22265  tngngp2  22266  xrsxmet  22420  xrge0gsumle  22444  metdstri  22462  xrhmeo  22553  lebnumlem3  22570  pcorevlem  22634  pi1xfrcnvlem  22664  clmabs  22691  cvsmuleqdivd  22742  rrxip  22986  rrxds  22989  minveclem4a  23009  pjthlem1  23016  ovolunlem1a  23071  mbfres2  23218  i1faddlem  23266  ibladdlem  23392  iblabs  23401  ditgsplit  23431  dvnres  23500  dveflem  23546  dveq0  23567  dvfsumabs  23590  itgsubstlem  23615  ply1divex  23700  dgrco  23835  plycjlem  23836  taylthlem1  23931  pserdv2  23988  abelthlem6  23994  abelthlem7  23996  tangtx  24061  abssinper  24074  sineq0  24077  explog  24144  reexplog  24145  eflogeq  24152  abslogle  24168  tanarg  24169  logtayl  24206  logtayl2  24208  relogbdiv  24317  ang180lem3  24341  affineequiv  24353  affineequiv2  24354  chordthmlem4  24362  chordthmlem5  24363  heron  24365  dcubic1lem  24370  dcubic2  24371  dcubic  24373  mcubic  24374  cubic2  24375  dquartlem1  24378  dquart  24380  quart1lem  24382  quartlem1  24384  quart  24388  acoscos  24420  atanlogaddlem  24440  atantayl2  24465  atantayl3  24466  birthdaylem2  24479  efrlim  24496  amgmlem  24516  logdifbnd  24520  emcllem3  24524  emcllem6  24527  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  gamigam  24579  lgamcvg2  24581  gamfac  24593  basellem3  24609  basellem8  24614  basellem9  24615  chtprm  24679  logfaclbnd  24747  perfect1  24753  bcp1ctr  24804  bclbnd  24805  bposlem1  24809  lgsdilem  24849  lgsdirnn0  24869  lgsdinn0  24870  gausslemma2dlem1a  24890  gausslemma2dlem4  24894  gausslemma2dlem5a  24895  lgseisenlem2  24901  lgsquadlem1  24905  2sqlem2  24943  mul2sq  24944  vmadivsum  24971  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem2  24979  dchrmusum2  24983  dchrvmasum2if  24986  dchrisum0lem2  25007  logsqvma2  25032  selberg3  25048  selberg4lem1  25049  pntrsumo1  25054  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntibndlem2  25080  pntlemk  25095  pntlemo  25096  ostth2lem4  25125  ostth3  25127  tgbtwndiff  25201  tgifscgr  25203  trgcgrg  25210  motcgr3  25240  tgbtwnconn1lem1  25267  tgbtwnconn1lem2  25268  ismir  25354  miriso  25365  midexlem  25387  ragmir  25395  footex  25413  colperpexlem3  25424  mideulem2  25426  midex  25429  opphllem3  25441  midcgr  25472  lmiisolem  25488  brbtwn2  25585  colinearalglem4  25589  axsegconlem1  25597  axpaschlem  25620  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  wwlkextwrd  26256  clwwlkn2  26303  clwlkisclwwlklem2a3  26309  clwlkisclwwlk2  26318  clwwlkel  26321  clwwlkfo  26325  clwwlkext2edg  26330  wwlkext2clwwlk  26331  frg2woteq  26587  extwwlkfablem1  26601  clwwlkextfrlem1  26603  numclwlk1lem2foa  26618  numclwlk1lem2fo  26622  numclwlk2lem2f  26630  grpoidinvlem2  26743  nvmtri  26910  cnnvm  26921  nvnd  26927  ipidsq  26949  ipnm  26950  ipipcj  26954  blocnilem  27043  ipasslem2  27071  dipsubdir  27087  hvaddsubval  27274  pjhthlem1  27634  pjspansn  27820  pjo  27914  unoplin  28163  adjadj  28179  hmoplin  28185  eigvec1  28205  lnopeqi  28251  nmcexi  28269  lnfnsubi  28289  riesz3i  28305  kbass6  28364  leoprf2  28370  leoprf  28371  pjnmopi  28391  mdslmd1lem1  28568  mdslmd1lem2  28569  superpos  28597  fgreu  28854  resf1o  28893  2sqmod  28979  gsummpt2d  29112  xrge0tsmseq  29118  subrgchr  29125  rhmdvd  29152  symgfcoeu  29176  psgnfzto1stlem  29181  psgnfzto1st  29186  madjusmdetlem2  29222  qtophaus  29231  pstmval  29266  mndpluscn  29300  qqhucn  29364  esumval  29435  gsumesum  29448  esumcst  29452  esumpcvgval  29467  oddpwdc  29743  eulerpartlemgvv  29765  probdif  29809  sgnmul  29931  signsvtn  29987  bnj1415  30360  derangen2  30410  subfaclefac  30412  subfaclim  30424  mrsubrn  30664  sinccvglem  30820  bcprod  30877  filnetlem4  31546  curunc  32561  ltflcei  32567  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  mblfinlem4  32619  ibladdnclem  32636  iblabsnc  32644  iblmulc2nc  32645  ftc1anclem6  32660  ftc1anclem8  32662  sdclem2  32708  ismtycnv  32771  heiborlem10  32789  lflvsass  33386  lkrscss  33403  eqlkr  33404  eqlkr3  33406  ldualvsdi2  33449  omllaw3  33550  cmtcomlemN  33553  cmtbr3N  33559  omlfh3N  33564  llnexchb2lem  34172  dalawlem7  34181  dalawlem11  34185  dalawlem12  34186  pol1N  34214  paddatclN  34253  4atexlemcnd  34376  ltrncoidN  34432  cdleme3b  34534  cdleme11  34575  cdleme15a  34579  cdleme22e  34650  cdleme22g  34654  cdlemg18b  34985  trlcoat  35029  cdlemk2  35138  cdlemk4  35140  cdlemki  35147  cdlemksv2  35153  cdlemk15  35161  cdlemk55a  35265  diainN  35364  dia2dimlem3  35373  dia2dimlem5  35375  dvhlveclem  35415  diaocN  35432  cdlemn4  35505  cdlemn8  35511  dihopelvalcpre  35555  dihmeetlem9N  35622  dih1dimatlem  35636  dihpN  35643  dochvalr3  35670  dochsat  35690  djhjlj  35710  dochdmm1  35717  dihjatcclem4  35728  dihjat1  35736  dihjat4  35740  dochsnkr2cl  35781  dochfl1  35783  lclkrlem2j  35823  mapdordlem2  35944  mapdrvallem2  35952  hdmap10  36150  mzpsubmpt  36324  irrapxlem3  36406  pellexlem6  36416  pell1234qrne0  36435  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell14qrdich  36451  pell1qrgaplem  36455  rmxluc  36519  rmyluc  36520  jm2.24nn  36544  jm2.18  36573  jm2.19lem2  36575  jm2.19lem3  36576  jm2.22  36580  jm2.23  36581  jm2.16nn0  36589  jm2.27c  36592  fnwe2lem2  36639  lmhmfgsplit  36674  hbtlem2  36713  relexpmulnn  37020  relexpmulg  37021  ntrclsneine0lem  37382  int-addassocd  37499  dvconstbi  37555  bccm1k  37563  binomcxplemnotnn0  37577  fmptsnxp  38343  wessf1ornlem  38366  founiiun0  38372  disjinfi  38375  projf1o  38381  lefldiveq  38446  lt4addmuld  38461  fzdifsuc2  38466  suplesup  38496  infrpge  38508  xrlexaddrp  38509  xralrple2  38511  infleinflem1  38527  fsumnncl  38638  limcperiod  38695  sumnnodd  38697  limcresiooub  38709  limcresioolb  38710  0ellimcdiv  38716  reclimc  38720  sinmulcos  38748  coskpi2  38749  divcncf  38769  cncfdmsn  38776  cncfiooicclem1  38779  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvmptdiv  38807  fperdvper  38808  dvmptresicc  38809  dvnmptdivc  38828  dvnxpaek  38832  dvnmul  38833  dvnprodlem1  38836  dvnprodlem3  38838  itgcoscmulx  38861  itgsincmulx  38866  itgspltprt  38871  itgiccshift  38872  itgperiod  38873  sublevolico  38877  volioof  38880  ovolsplit  38881  fvvolioof  38882  fvvolicof  38884  stoweidlem22  38915  stoweidlem32  38925  wallispilem5  38962  stirlinglem5  38971  dirkertrigeqlem2  38992  dirkertrigeq  38994  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem13  39013  fourierdlem16  39016  fourierdlem19  39019  fourierdlem21  39021  fourierdlem22  39022  fourierdlem28  39028  fourierdlem32  39032  fourierdlem33  39033  fourierdlem42  39042  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem56  39055  fourierdlem60  39059  fourierdlem61  39060  fourierdlem64  39063  fourierdlem66  39065  fourierdlem71  39070  fourierdlem73  39072  fourierdlem74  39073  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem80  39079  fourierdlem81  39080  fourierdlem83  39082  fourierdlem88  39087  fourierdlem92  39091  fourierdlem93  39092  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem109  39108  fourierdlem111  39110  fouriersw  39124  elaa2lem  39126  etransclem24  39151  etransclem25  39152  etransclem35  39162  etransclem46  39173  rrxdsfi  39181  rrndistlt  39186  rrxunitopnfi  39188  qndenserrnbl  39191  qndenserrnopnlem  39193  saldifcl2  39222  intsal  39224  sge0sn  39272  sge0ltfirp  39293  sge0iunmptlemre  39308  sge0fodjrnlem  39309  sge0isum  39320  sge0xaddlem1  39326  nnfoctbdjlem  39348  meassle  39356  ismeannd  39360  meadif  39372  meaiuninclem  39373  meaiininclem  39376  omeunile  39395  caragendifcl  39404  caratheodory  39418  isomenndlem  39420  ovnsubaddlem1  39460  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem2  39486  hoidmvle  39490  hoi2toco  39497  rrnmbl  39504  hoidifhspdmvle  39510  voncmpl  39511  hoiqssbl  39515  hspmbllem1  39516  hspmbllem2  39517  ovolval2lem  39533  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  hoimbl2  39555  vonhoire  39563  salpreimagelt  39595  salpreimalegt  39597  preimaioomnf  39606  smfres  39675  smfmullem1  39676  sigarcol  39702  sfprmdvdsmersenne  40058  lighneallem3  40062  lighneallem4  40065  nn0onn0exALTV  40147  nnsum3primesprm  40206  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  ccats1pfxeq  40284  pfxccatin12lem2  40287  pfxccatin12  40288  ushgredgedgaloop  40458  crctcsh1wlkn0lem6  41018  wwlksnextwrd  41103  clwlkclwwlklem2a3  41203  clwlkclwwlk2  41212  clwwlksel  41221  clwwlksfo  41225  clwwlksext2edg  41230  wwlksext2clwwlk  41231  eupth2eucrct  41385  av-clwwlkextfrlem1  41509  av-numclwlk1lem2foa  41521  av-numclwlk1lem2fo  41525  av-numclwlk2lem2f  41533  c0snmgmhm  41704  rngcifuestrc  41789  funcrngcsetc  41790  funcrngcsetcALT  41791  funcringcsetc  41827  funcringcsetcALTV2lem7  41834  funcringcsetclem7ALTV  41857  lincext3  42039  lincresunit3  42064  nn0onn0ex  42112  nnpw2pmod  42175  blennn0em1  42183  digexp  42199  dignn0ehalf  42209  nn0mulfsum  42216  recsec  42296  reccsc  42297  aacllem  42356  amgmlemALT  42358