Theorem eqtr2d 2775

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  3eqtrrd  2779  3eqtr2rd  2781  ifan  4583  ifor  4584  dfopif  4874  fnco  6686  fnsnfv  6987  nvocnv  7300  elovmpt3rab1  7692  onsucmin  7840  csbopeq1a  8073  oaabs2  8685  ecinxp  8830  resixpfo  8974  sbthlem3  9123  rankxpsuc  9919  fseqenlem2  10062  dfac2b  10168  isf32lem9  10398  compsscnvlem  10407  ttukeylem7  10552  fpwwe2lem10  10677  00id  11433  submul2  11700  mulsubfacd  11721  divadddiv  11979  infrenegsup  12248  xadd4d  13341  fzdifsuc  13620  fzval3  13769  fzoshftral  13819  ceim1l  13883  fldiv  13896  flmod  13921  intfrac  13922  modcyc2  13943  moddi  13976  uzrdgfni  13995  axdc4uzlem  14020  seqf1olem1  14078  seqf1olem2  14079  seqid2  14085  expnegz  14133  binom2sub  14255  binom3  14259  hashreshashfun  14474  ccatw2s1p2  14671  ccats1pfxeq  14748  pfxccatin12lem2  14765  pfxccatin12  14767  swrdccat3b  14774  cshweqrep  14855  2cshwcshw  14860  ccatco  14870  swrds2  14975  relexpsucnnr  15060  relexpaddnn  15086  reim  15144  mulre  15156  addcj  15183  absimle  15344  clim2ser  15687  isercoll2  15701  serf0  15713  iseralt  15717  summolem3  15746  isumclim3  15791  mptfzshft  15810  fsumrev  15811  fsum2mul  15821  incexc  15869  isumsplit  15872  mertenslem1  15916  fprodrev  16009  iprodclim3  16032  binomfallfaclem2  16072  ef4p  16145  tanval3  16166  efival  16184  sinmul  16204  bitsinvp1  16482  sadaddlem  16499  bitsshft  16508  smu01lem  16518  dfgcd2  16579  lcmgcdlem  16639  lcm1  16643  lcmfass  16679  eulerthlem2  16815  hashgcdeq  16822  powm2modprm  16836  pythagtriplem16  16863  pczpre  16880  pcqdiv  16890  pcadd  16922  pcfac  16932  prmreclem5  16953  4sqlem10  16980  4sqlem19  16996  vdwapun  17007  vdwlem1  17014  ramcl  17062  setsstruct  17209  strfvd  17234  strfv2d  17235  xpsff1o  17613  xpsrnbas  17617  2oppccomf  17771  oppcepi  17786  sscfn1  17864  sscfn2  17865  invfuc  18030  funcestrcsetclem7  18201  funcsetcestrclem7  18216  gsumsplit1r  18712  grpinvssd  19047  grpinvval2  19053  cycsubggend  19235  pmtrdifwrdellem2  19514  psgnunilem1  19525  psgnuni  19531  pgp0  19628  sylow1lem1  19630  sylow3lem2  19660  efgredleme  19775  efgcpbllemb  19787  frgpuptinv  19803  frgpup3lem  19809  gexexlem  19884  cyggenod  19916  gsumval3eu  19936  gsumval3  19939  gsumzaddlem  19953  dprd2db  20077  ablsimpgfindlem1  20141  ringinvdv  20430  c0snmgmhm  20478  rngcifuestrc  20655  funcrngcsetc  20656  funcrngcsetcALT  20657  funcringcsetc  20690  lss1d  20978  pwssplit1  21075  rhmqusnsg  21312  rngqiprnglin  21329  znzrh2  21581  regsumsupp  21657  ipassr2  21682  dsmmfi  21775  frlmlss  21788  frlmip  21815  frlmlbs  21834  frlmup3  21837  islindf4  21875  mplcoe3  22073  subrgascl  22107  evlseu  22124  psdadd  22184  ply1sclid  22306  ply1chr  22325  evls1addd  22390  evls1muld  22391  evls1vsca  22392  evls1maprhm  22395  evls1maplmhm  22396  evls1maprnss  22397  evl1maprhm  22398  1marepvmarrepid  22596  madurid  22665  smadiadetlem3  22689  mat2pmatghm  22751  pmatcollpwscmatlem1  22810  pm2mpmhmlem2  22840  cpmadurid  22888  cpmidgsumm2pm  22890  cpmadugsumlemB  22895  cayhamlem2  22905  ntrval2  23074  ordtuni  23213  cnclima  23291  cmpsub  23423  ptbasfi  23604  txbasval  23629  pt1hmeo  23829  alexsubALTlem1  24070  trust  24253  ussid  24284  ressuss  24286  ressprdsds  24396  imasdsf1olem  24398  setsms  24507  tmsxms  24514  tmsxpsmopn  24565  subgnm  24661  tngnm  24687  tngngp2  24688  xrsxmet  24844  xrge0gsumle  24868  metdstri  24886  xrhmeo  24990  lebnumlem3  25008  pcorevlem  25072  pi1xfrcnvlem  25102  clmabs  25129  cvsmuleqdivd  25180  rrxip  25437  rrxds  25440  rrxdsfi  25458  minveclem4a  25477  pjthlem1  25484  divcncf  25495  ovolunlem1a  25544  mbfres2  25693  i1faddlem  25741  ibladdlem  25869  iblabs  25878  ditgsplit  25910  dvmptresicc  25965  dvnres  25981  dvmptdiv  26026  dveflem  26031  dveq0  26053  dvfsumabs  26077  itgsubstlem  26103  ply1divex  26190  r1pid2  26215  dgrco  26329  plycjlem  26330  taylthlem1  26429  pserdv2  26488  abelthlem6  26494  abelthlem7  26496  tangtx  26561  abssinper  26577  sineq0  26580  explog  26650  reexplog  26651  eflogeq  26658  abslogle  26674  tanarg  26675  logtayl  26716  logtayl2  26718  relogbdiv  26836  ang180lem3  26868  affineequiv  26880  affineequiv2  26881  chordthmlem4  26892  chordthmlem5  26893  heron  26895  dcubic1lem  26900  dcubic2  26901  dcubic  26903  mcubic  26904  cubic2  26905  dquartlem1  26908  dquart  26910  quart1lem  26912  quartlem1  26914  quart  26918  acoscos  26950  atanlogaddlem  26970  atantayl2  26995  atantayl3  26996  birthdaylem2  27009  efrlim  27026  efrlimOLD  27027  amgmlem  27047  logdifbnd  27051  emcllem3  27055  emcllem6  27058  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  gamigam  27110  lgamcvg2  27112  gamfac  27124  basellem3  27140  basellem8  27145  basellem9  27146  chtprm  27210  logfaclbnd  27280  perfect1  27286  bcp1ctr  27337  bclbnd  27338  bposlem1  27342  lgsdilem  27382  lgsdirnn0  27402  lgsdinn0  27403  gausslemma2dlem1a  27423  gausslemma2dlem4  27427  gausslemma2dlem5a  27428  lgseisenlem2  27434  lgsquadlem1  27438  2sqlem2  27476  mul2sq  27477  2sqmod  27494  2sqnn0  27496  vmadivsum  27540  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrmusum2  27552  dchrvmasum2if  27555  dchrisum0lem2  27576  logsqvma2  27601  selberg3  27617  selberg4lem1  27618  pntrsumo1  27623  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem5  27639  pntibndlem2  27649  pntlemk  27664  pntlemo  27665  ostth2lem4  27694  ostth3  27696  subsfo  28109  negsval2  28110  sltonold  28297  noseqrdgfn  28326  addhalfcut  28433  tgbtwndiff  28528  tgifscgr  28530  trgcgrg  28537  motcgr3  28567  tgbtwnconn1lem1  28594  tgbtwnconn1lem2  28595  ismir  28681  miriso  28692  midexlem  28714  ragmir  28722  footexALT  28740  footexlem1  28741  footexlem2  28742  colperpexlem3  28754  mideulem2  28756  midex  28759  opphllem3  28771  midcgr  28802  lmiisolem  28818  brbtwn2  28934  colinearalglem4  28938  axsegconlem1  28946  axpaschlem  28969  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  ushgredgedgloop  29262  crctcshwlkn0lem6  29844  wwlknlsw  29876  wwlksnextwrd  29926  clwlkclwwlklem2a3  30022  clwlkclwwlk2  30031  clwwlkel  30074  clwwlkfo  30078  clwwlkext2edg  30084  eupth2eucrct  30245  numclwwlk2lem1lem  30370  numclwwlk1lem2fo  30386  numclwlk2lem2f  30405  grpoidinvlem2  30533  nvmtri  30699  cnnvm  30710  nvnd  30716  ipidsq  30738  ipnm  30739  ipipcj  30743  blocnilem  30832  ipasslem2  30860  dipsubdir  30876  hvaddsubval  31061  pjhthlem1  31419  pjspansn  31605  pjo  31699  unoplin  31948  adjadj  31964  hmoplin  31970  eigvec1  31990  lnopeqi  32036  nmcexi  32054  lnfnsubi  32074  riesz3i  32090  kbass6  32149  leoprf2  32155  leoprf  32156  pjnmopi  32176  mdslmd1lem1  32353  mdslmd1lem2  32354  superpos  32382  ifeq3da  32566  fgreu  32688  resf1o  32747  quad3d  32760  fprodex01  32831  ccatws1f1o  32920  wrdt2ind  32922  mndlactfo  33014  mndractfo  33016  gsummpt2d  33034  xrge0tsmseq  33049  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  symgfcoeu  33084  wrdpmtrlast  33095  psgnfzto1stlem  33102  psgnfzto1st  33107  cycpm2tr  33121  cycpmco2lem6  33133  cycpmco2lem7  33134  subrgchr  33226  elrgspnlem1  33231  elrgspnlem3  33233  rloccring  33256  rhmdvd  33327  qusrn  33416  nsgqusf1olem3  33422  rhmquskerlem  33432  elrspunsn  33436  mxidlirredi  33478  qsdrngi  33502  1arithidomlem1  33542  1arithidomlem2  33543  evls1subd  33576  r1pid2OLD  33608  resssra  33616  dimval  33627  dimvalfi  33628  lindsunlem  33651  dimkerim  33654  qusdimsum  33655  fedgmullem1  33656  extdg1id  33690  ply1annidllem  33708  algextdeglem4  33725  constrrtcc  33740  constrsslem  33745  madjusmdetlem2  33788  qtophaus  33796  zarclssn  33833  zarcmplem  33841  pstmval  33855  mndpluscn  33886  qqhucn  33954  esumval  34026  gsumesum  34039  esumcst  34043  esumpcvgval  34058  oddpwdc  34335  eulerpartlemgvv  34357  probdif  34401  sgnmul  34523  signsvtn  34577  actfunsnf1o  34597  reprpmtf1o  34619  hgt750lemd  34641  logdivsqrle  34643  hgt750lemg  34647  hgt750lemb  34649  bnj1415  35030  swrdrevpfx  35100  pfxwlk  35107  derangen2  35158  subfaclefac  35160  subfaclim  35172  satom  35340  fmla  35365  mrsubrn  35497  sinccvglem  35656  bcprod  35717  filnetlem4  36363  curunc  37588  ltflcei  37594  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  mblfinlem4  37646  ibladdnclem  37662  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem6  37684  ftc1anclem8  37686  sdclem2  37728  ismtycnv  37788  heiborlem10  37806  lflvsass  39062  lkrscss  39079  eqlkr  39080  eqlkr3  39082  ldualvsdi2  39125  omllaw3  39226  cmtcomlemN  39229  cmtbr3N  39235  omlfh3N  39240  llnexchb2lem  39850  dalawlem7  39859  dalawlem11  39863  dalawlem12  39864  pol1N  39892  paddatclN  39931  4atexlemcnd  40054  ltrncoidN  40110  cdleme3b  40211  cdleme11  40252  cdleme15a  40256  cdleme22e  40326  cdleme22g  40330  cdlemg18b  40661  trlcoat  40705  cdlemk2  40814  cdlemk4  40816  cdlemki  40823  cdlemksv2  40829  cdlemk15  40837  cdlemk55a  40941  diainN  41039  dia2dimlem3  41048  dia2dimlem5  41050  dvhlveclem  41090  diaocN  41107  cdlemn4  41180  cdlemn8  41186  dihopelvalcpre  41230  dihmeetlem9N  41297  dih1dimatlem  41311  dihpN  41318  dochvalr3  41345  dochsat  41365  djhjlj  41385  dochdmm1  41392  dihjatcclem4  41403  dihjat1  41411  dihjat4  41415  dochsnkr2cl  41456  dochfl1  41458  lclkrlem2j  41498  mapdordlem2  41619  mapdrvallem2  41627  hdmap10  41822  lcmineqlem12  42021  3lexlogpow5ineq5  42041  aks4d1p1  42057  primrootsunit1  42078  primrootscoprmpow  42080  posbezout  42081  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  aks6d1c1p7  42094  evl1gprodd  42098  hashscontpow1  42102  aks6d1c3  42104  aks6d1c2lem3  42107  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem3  42118  aks6d1c6lem1  42151  aks6d1c6isolem3  42157  aks6d1c6lem5  42158  bcle2d  42160  aks6d1c7lem1  42161  aks5lem3a  42170  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  aks5lem7  42181  nicomachus  42324  sumcubes  42325  cnreeu  42476  frlmvscadiccat  42492  grpcominv1  42494  riccrng1  42507  ricdrng1  42514  frlmsnic  42526  evlselv  42573  fsuppind  42576  flt4lem7  42645  negexpidd  42669  3cubeslem2  42672  3cubeslem3r  42674  mzpsubmpt  42730  irrapxlem3  42811  pellexlem6  42821  pell1234qrne0  42840  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell14qrdich  42856  pell1qrgaplem  42860  rmxluc  42924  rmyluc  42925  jm2.24nn  42947  jm2.18  42976  jm2.19lem2  42978  jm2.19lem3  42979  jm2.22  42983  jm2.23  42984  jm2.16nn0  42992  jm2.27c  42995  fnwe2lem2  43039  lmhmfgsplit  43074  hbtlem2  43112  onsucf1lem  43258  ofoafo  43345  naddcnffo  43353  naddwordnexlem4  43390  reabssgn  43625  relexpmulnn  43698  relexpmulg  43699  ntrclsneine0lem  44053  int-addassocd  44163  dvconstbi  44329  bccm1k  44337  binomcxplemnotnn0  44351  fmptsnxp  45111  wessf1ornlem  45127  projf1o  45139  infnsuprnmpt  45194  lefldiveq  45242  lt4addmuld  45256  fzdifsuc2  45260  suplesup  45288  infrpge  45300  xrlexaddrp  45301  xralrple2  45303  infleinflem1  45319  supminfrnmpt  45394  supminfxr2  45418  fsumnncl  45527  limcperiod  45583  sumnnodd  45585  limcresiooub  45597  limcresioolb  45598  0ellimcdiv  45604  reclimc  45608  limsupval3  45647  limsupequzmpt2  45673  liminfval5  45720  limsupresxr  45721  liminfresxr  45722  liminfvalxr  45738  liminfequzmpt2  45746  climliminflimsupd  45756  liminfltlem  45759  liminflbuz2  45770  sinmulcos  45820  coskpi2  45821  cncfdmsn  45845  cncfiooicclem1  45848  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  fperdvper  45874  dvnmptdivc  45893  dvnxpaek  45897  dvnmul  45898  dvnprodlem1  45901  dvnprodlem3  45903  itgcoscmulx  45924  itgsincmulx  45929  itgspltprt  45934  itgiccshift  45935  itgperiod  45936  sublevolico  45939  volioof  45942  ovolsplit  45943  fvvolioof  45944  fvvolicof  45946  stoweidlem22  45977  stoweidlem32  45987  wallispilem5  46024  stirlinglem5  46033  dirkertrigeqlem2  46054  dirkertrigeq  46056  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem13  46075  fourierdlem16  46078  fourierdlem19  46081  fourierdlem21  46083  fourierdlem22  46084  fourierdlem28  46090  fourierdlem32  46094  fourierdlem33  46095  fourierdlem42  46104  fourierdlem47  46108  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem56  46117  fourierdlem60  46121  fourierdlem61  46122  fourierdlem64  46125  fourierdlem66  46127  fourierdlem71  46132  fourierdlem73  46134  fourierdlem74  46135  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem80  46141  fourierdlem81  46142  fourierdlem83  46144  fourierdlem88  46149  fourierdlem92  46153  fourierdlem93  46154  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem109  46170  fourierdlem111  46172  fouriersw  46186  elaa2lem  46188  etransclem24  46213  etransclem25  46214  etransclem35  46224  etransclem46  46235  rrndistlt  46245  rrxunitopnfi  46247  qndenserrnbl  46250  qndenserrnopnlem  46252  saldifcl2  46283  intsal  46285  sge0sn  46334  sge0ltfirp  46355  sge0iunmptlemre  46370  sge0fodjrnlem  46371  sge0isum  46382  sge0xaddlem1  46388  nnfoctbdjlem  46410  meassle  46418  ismeannd  46422  meadif  46434  meaiuninclem  46435  meaiininclem  46441  omeunile  46460  caragendifcl  46469  caratheodory  46483  isomenndlem  46485  ovnsubaddlem1  46525  hoidmv1lelem2  46547  hoidmv1le  46549  hoidmvlelem2  46551  hoidmvle  46555  hoi2toco  46562  rrnmbl  46569  hoidifhspdmvle  46575  voncmpl  46576  hoiqssbl  46580  hspmbllem1  46581  hspmbllem2  46582  ovolval2lem  46598  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  hoimbl2  46620  vonhoire  46627  salpreimagelt  46662  salpreimalegt  46664  preimaioomnf  46674  smfres  46745  smfmullem1  46746  smflimmpt  46765  smfsupmpt  46770  smfinfmpt  46774  smflimsupmpt  46784  smfliminflem  46785  smfliminfmpt  46787  sigarcol  46819  f1oresf1o  47239  elsprel  47399  prproropf1o  47431  paireqne  47435  sfprmdvdsmersenne  47527  lighneallem3  47531  lighneallem4  47534  nn0onn0exALTV  47623  nnsum3primesprm  47714  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  isuspgrim0lem  47808  clnbgrgrimlem  47838  uspgrlimlem3  47892  uspgrlimlem4  47893  gpgedgvtx0  47953  gpgedgvtx1  47954  funcringcsetcALTV2lem7  48139  funcringcsetclem7ALTV  48162  lincext3  48301  lincresunit3  48326  nn0onn0ex  48372  nnpw2pmod  48432  blennn0em1  48440  digexp  48456  dignn0ehalf  48466  nn0mulfsum  48473  itcovalpclem1  48519  eenglngeehlnmlem2  48587  rrx2vlinest  48590  line2  48601  itschlc0xyqsol  48616  itsclinecirc0b  48623  toplatjoin  48790  toplatmeet  48791  upeu2lem  48807  upciclem3  48813  recsec  48986  reccsc  48987  aacllem  49031  amgmlemALT  49033