Theorem eqtr2d 2767

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  3eqtrrd  2771  3eqtr2rd  2773  ifan  4524  ifor  4525  dfopif  4817  fnco  6594  fnsnfv  6896  nvocnv  7210  elovmpt3rab1  7601  onsucmin  7746  csbopeq1a  7977  oaabs2  8559  ecinxp  8711  resixpfo  8855  sbthlem3  8997  rankxpsuc  9770  fseqenlem2  9911  dfac2b  10017  isf32lem9  10247  compsscnvlem  10256  ttukeylem7  10401  fpwwe2lem10  10526  00id  11283  submul2  11552  mulsubfacd  11573  divadddiv  11831  infrenegsup  12100  xadd4d  13197  fzdifsuc  13479  fzval3  13629  fzoshftral  13682  ceim1l  13746  fldiv  13759  flmod  13784  intfrac  13785  modcyc2  13806  modaddb  13808  moddi  13841  uzrdgfni  13860  axdc4uzlem  13885  seqf1olem1  13943  seqf1olem2  13944  seqid2  13950  expnegz  13998  binom2sub  14122  binom3  14126  hashreshashfun  14341  ccatw2s1p2  14540  ccats1pfxeq  14616  pfxccatin12lem2  14633  pfxccatin12  14635  swrdccat3b  14642  cshweqrep  14723  2cshwcshw  14727  ccatco  14737  swrds2  14842  relexpsucnnr  14927  relexpaddnn  14953  reim  15011  mulre  15023  addcj  15050  absimle  15211  clim2ser  15557  isercoll2  15571  serf0  15583  iseralt  15587  summolem3  15616  isumclim3  15661  mptfzshft  15680  fsumrev  15681  fsum2mul  15691  incexc  15739  isumsplit  15742  mertenslem1  15786  fprodrev  15879  iprodclim3  15902  binomfallfaclem2  15942  ef4p  16017  tanval3  16038  efival  16056  sinmul  16076  bitsinvp1  16355  sadaddlem  16372  bitsshft  16381  smu01lem  16391  dfgcd2  16452  lcmgcdlem  16512  lcm1  16516  lcmfass  16552  eulerthlem2  16688  hashgcdeq  16696  powm2modprm  16710  pythagtriplem16  16737  pczpre  16754  pcqdiv  16764  pcadd  16796  pcfac  16806  prmreclem5  16827  4sqlem10  16854  4sqlem19  16870  vdwapun  16881  vdwlem1  16888  ramcl  16936  setsstruct  17082  strfvd  17106  strfv2d  17107  xpsff1o  17466  xpsrnbas  17470  2oppccomf  17626  oppcepi  17641  sscfn1  17719  sscfn2  17720  invfuc  17879  funcestrcsetclem7  18047  funcsetcestrclem7  18062  gsumsplit1r  18590  grpinvssd  18925  grpinvval2  18931  cycsubggend  19112  pmtrdifwrdellem2  19389  psgnunilem1  19400  psgnuni  19406  pgp0  19503  sylow1lem1  19505  sylow3lem2  19535  efgredleme  19650  efgcpbllemb  19662  frgpuptinv  19678  frgpup3lem  19684  gexexlem  19759  cyggenod  19791  gsumval3eu  19811  gsumval3  19814  gsumzaddlem  19828  dprd2db  19952  ablsimpgfindlem1  20016  ringinvdv  20327  c0snmgmhm  20375  rngcifuestrc  20549  funcrngcsetc  20550  funcrngcsetcALT  20551  funcringcsetc  20584  lss1d  20891  pwssplit1  20988  rhmqusnsg  21217  rngqiprnglin  21234  znzrh2  21477  regsumsupp  21554  ipassr2  21579  dsmmfi  21670  frlmlss  21683  frlmip  21710  frlmlbs  21729  frlmup3  21732  islindf4  21770  mplcoe3  21968  subrgascl  21996  evlseu  22013  psdadd  22073  ply1sclid  22197  ply1chr  22216  evls1addd  22281  evls1muld  22282  evls1vsca  22283  evls1maprhm  22286  evls1maplmhm  22287  evls1maprnss  22288  evl1maprhm  22289  1marepvmarrepid  22485  madurid  22554  smadiadetlem3  22578  mat2pmatghm  22640  pmatcollpwscmatlem1  22699  pm2mpmhmlem2  22729  cpmadurid  22777  cpmidgsumm2pm  22779  cpmadugsumlemB  22784  cayhamlem2  22794  ntrval2  22961  ordtuni  23100  cnclima  23178  cmpsub  23310  ptbasfi  23491  txbasval  23516  pt1hmeo  23716  alexsubALTlem1  23957  trust  24139  ussid  24170  ressuss  24172  ressprdsds  24281  imasdsf1olem  24283  setsms  24390  tmsxms  24396  tmsxpsmopn  24447  subgnm  24543  tngnm  24561  tngngp2  24562  xrsxmet  24720  xrge0gsumle  24744  metdstri  24762  xrhmeo  24866  lebnumlem3  24884  pcorevlem  24948  pi1xfrcnvlem  24978  clmabs  25005  cvsmuleqdivd  25056  rrxip  25312  rrxds  25315  rrxdsfi  25333  minveclem4a  25352  pjthlem1  25359  divcncf  25370  ovolunlem1a  25419  mbfres2  25568  i1faddlem  25616  ibladdlem  25743  iblabs  25752  ditgsplit  25784  dvmptresicc  25839  dvnres  25855  dvmptdiv  25900  dveflem  25905  dveq0  25927  dvfsumabs  25951  itgsubstlem  25977  ply1divex  26064  r1pid2  26089  dgrco  26203  plycjlem  26204  taylthlem1  26303  pserdv2  26362  abelthlem6  26368  abelthlem7  26370  tangtx  26436  abssinper  26452  sineq0  26455  explog  26525  reexplog  26526  eflogeq  26533  abslogle  26549  tanarg  26550  logtayl  26591  logtayl2  26593  relogbdiv  26711  ang180lem3  26743  affineequiv  26755  affineequiv2  26756  chordthmlem4  26767  chordthmlem5  26768  heron  26770  dcubic1lem  26775  dcubic2  26776  dcubic  26778  mcubic  26779  cubic2  26780  dquartlem1  26783  dquart  26785  quart1lem  26787  quartlem1  26789  quart  26793  acoscos  26825  atanlogaddlem  26845  atantayl2  26870  atantayl3  26871  birthdaylem2  26884  efrlim  26901  efrlimOLD  26902  amgmlem  26922  logdifbnd  26926  emcllem3  26930  emcllem6  26933  lgamgulmlem2  26962  lgamgulmlem3  26963  lgamgulmlem4  26964  lgamgulmlem5  26965  gamigam  26985  lgamcvg2  26987  gamfac  26999  basellem3  27015  basellem8  27020  basellem9  27021  chtprm  27085  logfaclbnd  27155  perfect1  27161  bcp1ctr  27212  bclbnd  27213  bposlem1  27217  lgsdilem  27257  lgsdirnn0  27277  lgsdinn0  27278  gausslemma2dlem1a  27298  gausslemma2dlem4  27302  gausslemma2dlem5a  27303  lgseisenlem2  27309  lgsquadlem1  27313  2sqlem2  27351  mul2sq  27352  2sqmod  27369  2sqnn0  27371  vmadivsum  27415  rpvmasumlem  27420  dchrisumlem1  27422  dchrisumlem2  27423  dchrmusum2  27427  dchrvmasum2if  27430  dchrisum0lem2  27451  logsqvma2  27476  selberg3  27492  selberg4lem1  27493  pntrsumo1  27498  pntrlog2bndlem2  27511  pntrlog2bndlem3  27512  pntrlog2bndlem5  27514  pntibndlem2  27524  pntlemk  27539  pntlemo  27540  ostth2lem4  27569  ostth3  27571  subsfo  28000  negsval2  28001  sltonold  28193  noseqrdgfn  28231  n0sfincut  28277  addhalfcut  28374  zs12half  28385  tgbtwndiff  28479  tgifscgr  28481  trgcgrg  28488  motcgr3  28518  tgbtwnconn1lem1  28545  tgbtwnconn1lem2  28546  ismir  28632  miriso  28643  midexlem  28665  ragmir  28673  footexALT  28691  footexlem1  28692  footexlem2  28693  colperpexlem3  28705  mideulem2  28707  midex  28710  opphllem3  28722  midcgr  28753  lmiisolem  28769  brbtwn2  28878  colinearalglem4  28882  axsegconlem1  28890  axpaschlem  28913  axcontlem4  28940  axcontlem7  28943  axcontlem8  28944  ushgredgedgloop  29204  crctcshwlkn0lem6  29788  wwlknlsw  29820  wwlksnextwrd  29870  clwlkclwwlklem2a3  29966  clwlkclwwlk2  29975  clwwlkel  30018  clwwlkfo  30022  clwwlkext2edg  30028  eupth2eucrct  30189  numclwwlk2lem1lem  30314  numclwwlk1lem2fo  30330  numclwlk2lem2f  30349  grpoidinvlem2  30477  nvmtri  30643  cnnvm  30654  nvnd  30660  ipidsq  30682  ipnm  30683  ipipcj  30687  blocnilem  30776  ipasslem2  30804  dipsubdir  30820  hvaddsubval  31005  pjhthlem1  31363  pjspansn  31549  pjo  31643  unoplin  31892  adjadj  31908  hmoplin  31914  eigvec1  31934  lnopeqi  31980  nmcexi  31998  lnfnsubi  32018  riesz3i  32034  kbass6  32093  leoprf2  32099  leoprf  32100  pjnmopi  32120  mdslmd1lem1  32297  mdslmd1lem2  32298  superpos  32326  ifeq3da  32518  fgreu  32646  cocnvf1o  32704  resf1o  32705  quad3d  32725  fprodex01  32800  sgnmul  32810  ccatws1f1o  32924  wrdt2ind  32926  mndlactfo  33000  mndractfo  33002  gsummpt2d  33021  xrge0tsmseq  33036  gsumwrd2dccatlem  33038  gsumwrd2dccat  33039  symgfcoeu  33043  wrdpmtrlast  33054  psgnfzto1stlem  33061  psgnfzto1st  33066  cycpm2tr  33080  cycpmco2lem6  33092  cycpmco2lem7  33093  subrgchr  33196  elrgspnlem1  33201  elrgspnlem3  33203  elrgspnsubrunlem1  33206  rloccring  33229  rhmdvd  33281  qusrn  33366  nsgqusf1olem3  33372  rhmquskerlem  33382  elrspunsn  33386  mxidlirredi  33428  qsdrngi  33452  1arithidomlem1  33492  1arithidomlem2  33493  evls1subd  33527  r1pid2OLD  33561  resssra  33591  dimval  33605  dimvalfi  33606  lindsunlem  33629  dimkerim  33632  qusdimsum  33633  fedgmullem1  33634  extdg1id  33671  fldextrspunlsplem  33678  fldextrspunlsp  33679  fldextrspunlem1  33680  fldextrspundgdvds  33686  extdgfialglem1  33697  extdgfialglem2  33698  ply1annidllem  33706  algextdeglem4  33725  constrrtcc  33740  constrsslem  33746  constrresqrtcl  33782  cos9thpiminplylem2  33788  cos9thpiminply  33793  madjusmdetlem2  33833  qtophaus  33841  zarclssn  33878  zarcmplem  33886  pstmval  33900  mndpluscn  33931  qqhucn  33997  esumval  34051  gsumesum  34064  esumcst  34068  esumpcvgval  34083  oddpwdc  34359  eulerpartlemgvv  34381  probdif  34425  signsvtn  34589  actfunsnf1o  34609  reprpmtf1o  34631  hgt750lemd  34653  logdivsqrle  34655  hgt750lemg  34659  hgt750lemb  34661  bnj1415  35042  swrdrevpfx  35153  pfxwlk  35160  derangen2  35210  subfaclefac  35212  subfaclim  35224  satom  35392  fmla  35417  mrsubrn  35549  sinccvglem  35708  bcprod  35774  filnetlem4  36415  curunc  37642  ltflcei  37648  matunitlindflem1  37656  matunitlindflem2  37657  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem24  37684  mblfinlem4  37700  ibladdnclem  37716  iblabsnc  37724  iblmulc2nc  37725  ftc1anclem6  37738  ftc1anclem8  37740  sdclem2  37782  ismtycnv  37842  heiborlem10  37860  lflvsass  39120  lkrscss  39137  eqlkr  39138  eqlkr3  39140  ldualvsdi2  39183  omllaw3  39284  cmtcomlemN  39287  cmtbr3N  39293  omlfh3N  39298  llnexchb2lem  39907  dalawlem7  39916  dalawlem11  39920  dalawlem12  39921  pol1N  39949  paddatclN  39988  4atexlemcnd  40111  ltrncoidN  40167  cdleme3b  40268  cdleme11  40309  cdleme15a  40313  cdleme22e  40383  cdleme22g  40387  cdlemg18b  40718  trlcoat  40762  cdlemk2  40871  cdlemk4  40873  cdlemki  40880  cdlemksv2  40886  cdlemk15  40894  cdlemk55a  40998  diainN  41096  dia2dimlem3  41105  dia2dimlem5  41107  dvhlveclem  41147  diaocN  41164  cdlemn4  41237  cdlemn8  41243  dihopelvalcpre  41287  dihmeetlem9N  41354  dih1dimatlem  41368  dihpN  41375  dochvalr3  41402  dochsat  41422  djhjlj  41442  dochdmm1  41449  dihjatcclem4  41460  dihjat1  41468  dihjat4  41472  dochsnkr2cl  41513  dochfl1  41515  lclkrlem2j  41555  mapdordlem2  41676  mapdrvallem2  41684  hdmap10  41879  lcmineqlem12  42073  3lexlogpow5ineq5  42093  aks4d1p1  42109  primrootsunit1  42130  primrootscoprmpow  42132  posbezout  42133  aks6d1c1p3  42143  aks6d1c1p4  42144  aks6d1c1p5  42145  aks6d1c1p7  42146  evl1gprodd  42150  hashscontpow1  42154  aks6d1c3  42156  aks6d1c2lem3  42159  aks6d1c2lem4  42160  aks6d1c2  42163  aks6d1c5lem3  42170  aks6d1c6lem1  42203  aks6d1c6isolem3  42209  aks6d1c6lem5  42210  bcle2d  42212  aks6d1c7lem1  42213  aks5lem3a  42222  grpods  42227  unitscyglem1  42228  unitscyglem2  42229  unitscyglem4  42231  unitscyglem5  42232  aks5lem7  42233  nicomachus  42345  sumcubes  42346  cnreeu  42523  frlmvscadiccat  42539  grpcominv1  42541  riccrng1  42554  ricdrng1  42561  frlmsnic  42573  evlselv  42620  fsuppind  42623  flt4lem7  42692  negexpidd  42715  3cubeslem2  42718  3cubeslem3r  42720  mzpsubmpt  42776  irrapxlem3  42857  pellexlem6  42867  pell1234qrne0  42886  pell1234qrreccl  42887  pell1234qrmulcl  42888  pell14qrdich  42902  pell1qrgaplem  42906  rmxluc  42969  rmyluc  42970  jm2.24nn  42992  jm2.18  43021  jm2.19lem2  43023  jm2.19lem3  43024  jm2.22  43028  jm2.23  43029  jm2.16nn0  43037  jm2.27c  43040  fnwe2lem2  43084  lmhmfgsplit  43119  hbtlem2  43157  onsucf1lem  43302  ofoafo  43389  naddcnffo  43397  naddwordnexlem4  43434  reabssgn  43669  relexpmulnn  43742  relexpmulg  43743  ntrclsneine0lem  44097  int-addassocd  44207  dvconstbi  44367  bccm1k  44375  binomcxplemnotnn0  44389  fmptsnxp  45206  wessf1ornlem  45222  projf1o  45234  infnsuprnmpt  45287  lefldiveq  45333  lt4addmuld  45347  fzdifsuc2  45351  suplesup  45378  infrpge  45390  xrlexaddrp  45391  xralrple2  45393  infleinflem1  45408  supminfrnmpt  45483  supminfxr2  45507  fsumnncl  45612  limcperiod  45668  sumnnodd  45670  limcresiooub  45680  limcresioolb  45681  0ellimcdiv  45687  reclimc  45691  limsupval3  45730  limsupequzmpt2  45756  liminfval5  45803  limsupresxr  45804  liminfresxr  45805  liminfvalxr  45821  liminfequzmpt2  45829  climliminflimsupd  45839  liminfltlem  45842  liminflbuz2  45853  sinmulcos  45903  coskpi2  45904  cncfdmsn  45928  cncfiooicclem1  45931  fprodsubrecnncnvlem  45945  fprodaddrecnncnvlem  45947  fperdvper  45957  dvnmptdivc  45976  dvnxpaek  45980  dvnmul  45981  dvnprodlem1  45984  dvnprodlem3  45986  itgcoscmulx  46007  itgsincmulx  46012  itgspltprt  46017  itgiccshift  46018  itgperiod  46019  sublevolico  46022  volioof  46025  ovolsplit  46026  fvvolioof  46027  fvvolicof  46029  stoweidlem22  46060  stoweidlem32  46070  wallispilem5  46107  stirlinglem5  46116  dirkertrigeqlem2  46137  dirkertrigeq  46139  dirkercncflem1  46141  dirkercncflem2  46142  dirkercncflem4  46144  fourierdlem13  46158  fourierdlem16  46161  fourierdlem19  46164  fourierdlem21  46166  fourierdlem22  46167  fourierdlem28  46173  fourierdlem32  46177  fourierdlem33  46178  fourierdlem42  46187  fourierdlem47  46191  fourierdlem48  46192  fourierdlem49  46193  fourierdlem50  46194  fourierdlem56  46200  fourierdlem60  46204  fourierdlem61  46205  fourierdlem64  46208  fourierdlem66  46210  fourierdlem71  46215  fourierdlem73  46217  fourierdlem74  46218  fourierdlem76  46220  fourierdlem78  46222  fourierdlem79  46223  fourierdlem80  46224  fourierdlem81  46225  fourierdlem83  46227  fourierdlem88  46232  fourierdlem92  46236  fourierdlem93  46237  fourierdlem97  46241  fourierdlem101  46245  fourierdlem103  46247  fourierdlem104  46248  fourierdlem109  46253  fourierdlem111  46255  fouriersw  46269  elaa2lem  46271  etransclem24  46296  etransclem25  46297  etransclem35  46307  etransclem46  46318  rrndistlt  46328  rrxunitopnfi  46330  qndenserrnbl  46333  qndenserrnopnlem  46335  saldifcl2  46366  intsal  46368  sge0sn  46417  sge0ltfirp  46438  sge0iunmptlemre  46453  sge0fodjrnlem  46454  sge0isum  46465  sge0xaddlem1  46471  nnfoctbdjlem  46493  meassle  46501  ismeannd  46505  meadif  46517  meaiuninclem  46518  meaiininclem  46524  omeunile  46543  caragendifcl  46552  caratheodory  46566  isomenndlem  46568  ovnsubaddlem1  46608  hoidmv1lelem2  46630  hoidmv1le  46632  hoidmvlelem2  46634  hoidmvle  46638  hoi2toco  46645  rrnmbl  46652  hoidifhspdmvle  46658  voncmpl  46659  hoiqssbl  46663  hspmbllem1  46664  hspmbllem2  46665  ovolval2lem  46681  ovolval5lem2  46691  ovnovollem1  46694  ovnovollem2  46695  hoimbl2  46703  vonhoire  46710  salpreimagelt  46745  salpreimalegt  46747  preimaioomnf  46757  smfres  46828  smfmullem1  46829  smflimmpt  46848  smfsupmpt  46853  smfinfmpt  46857  smflimsupmpt  46867  smfliminflem  46868  smfliminfmpt  46870  sigarcol  46902  f1oresf1o  47321  elsprel  47506  prproropf1o  47538  paireqne  47542  sfprmdvdsmersenne  47634  lighneallem3  47638  lighneallem4  47641  nn0onn0exALTV  47730  nnsum3primesprm  47821  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  isuspgrim0lem  47924  clnbgrgrimlem  47964  uspgrlimlem3  48021  uspgrlimlem4  48022  gpgedgvtx0  48092  gpgedgvtx1  48093  funcringcsetcALTV2lem7  48327  funcringcsetclem7ALTV  48350  lincext3  48488  lincresunit3  48513  nn0onn0ex  48555  nnpw2pmod  48615  blennn0em1  48623  digexp  48639  dignn0ehalf  48649  nn0mulfsum  48656  itcovalpclem1  48702  eenglngeehlnmlem2  48770  rrx2vlinest  48773  line2  48784  itschlc0xyqsol  48799  itsclinecirc0b  48806  toplatjoin  49033  toplatmeet  49034  upeu2lem  49060  oppff1o  49181  imaf1co  49187  upciclem3  49200  natoppfb  49263  oppcthinco  49471  oppcthinendcALT  49473  lmddu  49699  recsec  49788  reccsc  49789  aacllem  49833  amgmlemALT  49835