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  4532  ifor  4533  dfopif  4824  fnco  6604  fnsnfv  6906  nvocnv  7222  elovmpt3rab1  7613  onsucmin  7760  csbopeq1a  7992  oaabs2  8574  ecinxp  8726  resixpfo  8870  sbthlem3  9013  rankxpsuc  9797  fseqenlem2  9938  dfac2b  10044  isf32lem9  10274  compsscnvlem  10283  ttukeylem7  10428  fpwwe2lem10  10553  00id  11309  submul2  11578  mulsubfacd  11599  divadddiv  11857  infrenegsup  12126  xadd4d  13223  fzdifsuc  13505  fzval3  13655  fzoshftral  13705  ceim1l  13769  fldiv  13782  flmod  13807  intfrac  13808  modcyc2  13829  modaddb  13831  moddi  13864  uzrdgfni  13883  axdc4uzlem  13908  seqf1olem1  13966  seqf1olem2  13967  seqid2  13973  expnegz  14021  binom2sub  14145  binom3  14149  hashreshashfun  14364  ccatw2s1p2  14562  ccats1pfxeq  14638  pfxccatin12lem2  14655  pfxccatin12  14657  swrdccat3b  14664  cshweqrep  14745  2cshwcshw  14750  ccatco  14760  swrds2  14865  relexpsucnnr  14950  relexpaddnn  14976  reim  15034  mulre  15046  addcj  15073  absimle  15234  clim2ser  15580  isercoll2  15594  serf0  15606  iseralt  15610  summolem3  15639  isumclim3  15684  mptfzshft  15703  fsumrev  15704  fsum2mul  15714  incexc  15762  isumsplit  15765  mertenslem1  15809  fprodrev  15902  iprodclim3  15925  binomfallfaclem2  15965  ef4p  16040  tanval3  16061  efival  16079  sinmul  16099  bitsinvp1  16378  sadaddlem  16395  bitsshft  16404  smu01lem  16414  dfgcd2  16475  lcmgcdlem  16535  lcm1  16539  lcmfass  16575  eulerthlem2  16711  hashgcdeq  16719  powm2modprm  16733  pythagtriplem16  16760  pczpre  16777  pcqdiv  16787  pcadd  16819  pcfac  16829  prmreclem5  16850  4sqlem10  16877  4sqlem19  16893  vdwapun  16904  vdwlem1  16911  ramcl  16959  setsstruct  17105  strfvd  17129  strfv2d  17130  xpsff1o  17489  xpsrnbas  17493  2oppccomf  17649  oppcepi  17664  sscfn1  17742  sscfn2  17743  invfuc  17902  funcestrcsetclem7  18070  funcsetcestrclem7  18085  gsumsplit1r  18579  grpinvssd  18914  grpinvval2  18920  cycsubggend  19102  pmtrdifwrdellem2  19379  psgnunilem1  19390  psgnuni  19396  pgp0  19493  sylow1lem1  19495  sylow3lem2  19525  efgredleme  19640  efgcpbllemb  19652  frgpuptinv  19668  frgpup3lem  19674  gexexlem  19749  cyggenod  19781  gsumval3eu  19801  gsumval3  19804  gsumzaddlem  19818  dprd2db  19942  ablsimpgfindlem1  20006  ringinvdv  20317  c0snmgmhm  20365  rngcifuestrc  20542  funcrngcsetc  20543  funcrngcsetcALT  20544  funcringcsetc  20577  lss1d  20884  pwssplit1  20981  rhmqusnsg  21210  rngqiprnglin  21227  znzrh2  21470  regsumsupp  21547  ipassr2  21572  dsmmfi  21663  frlmlss  21676  frlmip  21703  frlmlbs  21722  frlmup3  21725  islindf4  21763  mplcoe3  21961  subrgascl  21989  evlseu  22006  psdadd  22066  ply1sclid  22190  ply1chr  22209  evls1addd  22274  evls1muld  22275  evls1vsca  22276  evls1maprhm  22279  evls1maplmhm  22280  evls1maprnss  22281  evl1maprhm  22282  1marepvmarrepid  22478  madurid  22547  smadiadetlem3  22571  mat2pmatghm  22633  pmatcollpwscmatlem1  22692  pm2mpmhmlem2  22722  cpmadurid  22770  cpmidgsumm2pm  22772  cpmadugsumlemB  22777  cayhamlem2  22787  ntrval2  22954  ordtuni  23093  cnclima  23171  cmpsub  23303  ptbasfi  23484  txbasval  23509  pt1hmeo  23709  alexsubALTlem1  23950  trust  24133  ussid  24164  ressuss  24166  ressprdsds  24275  imasdsf1olem  24277  setsms  24384  tmsxms  24390  tmsxpsmopn  24441  subgnm  24537  tngnm  24555  tngngp2  24556  xrsxmet  24714  xrge0gsumle  24738  metdstri  24756  xrhmeo  24860  lebnumlem3  24878  pcorevlem  24942  pi1xfrcnvlem  24972  clmabs  24999  cvsmuleqdivd  25050  rrxip  25306  rrxds  25309  rrxdsfi  25327  minveclem4a  25346  pjthlem1  25353  divcncf  25364  ovolunlem1a  25413  mbfres2  25562  i1faddlem  25610  ibladdlem  25737  iblabs  25746  ditgsplit  25778  dvmptresicc  25833  dvnres  25849  dvmptdiv  25894  dveflem  25899  dveq0  25921  dvfsumabs  25945  itgsubstlem  25971  ply1divex  26058  r1pid2  26083  dgrco  26197  plycjlem  26198  taylthlem1  26297  pserdv2  26356  abelthlem6  26362  abelthlem7  26364  tangtx  26430  abssinper  26446  sineq0  26449  explog  26519  reexplog  26520  eflogeq  26527  abslogle  26543  tanarg  26544  logtayl  26585  logtayl2  26587  relogbdiv  26705  ang180lem3  26737  affineequiv  26749  affineequiv2  26750  chordthmlem4  26761  chordthmlem5  26762  heron  26764  dcubic1lem  26769  dcubic2  26770  dcubic  26772  mcubic  26773  cubic2  26774  dquartlem1  26777  dquart  26779  quart1lem  26781  quartlem1  26783  quart  26787  acoscos  26819  atanlogaddlem  26839  atantayl2  26864  atantayl3  26865  birthdaylem2  26878  efrlim  26895  efrlimOLD  26896  amgmlem  26916  logdifbnd  26920  emcllem3  26924  emcllem6  26927  lgamgulmlem2  26956  lgamgulmlem3  26957  lgamgulmlem4  26958  lgamgulmlem5  26959  gamigam  26979  lgamcvg2  26981  gamfac  26993  basellem3  27009  basellem8  27014  basellem9  27015  chtprm  27079  logfaclbnd  27149  perfect1  27155  bcp1ctr  27206  bclbnd  27207  bposlem1  27211  lgsdilem  27251  lgsdirnn0  27271  lgsdinn0  27272  gausslemma2dlem1a  27292  gausslemma2dlem4  27296  gausslemma2dlem5a  27297  lgseisenlem2  27303  lgsquadlem1  27307  2sqlem2  27345  mul2sq  27346  2sqmod  27363  2sqnn0  27365  vmadivsum  27409  rpvmasumlem  27414  dchrisumlem1  27416  dchrisumlem2  27417  dchrmusum2  27421  dchrvmasum2if  27424  dchrisum0lem2  27445  logsqvma2  27470  selberg3  27486  selberg4lem1  27487  pntrsumo1  27492  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem5  27508  pntibndlem2  27518  pntlemk  27533  pntlemo  27534  ostth2lem4  27563  ostth3  27565  subsfo  27992  negsval2  27993  sltonold  28185  noseqrdgfn  28223  n0sfincut  28269  addhalfcut  28365  zs12half  28375  tgbtwndiff  28469  tgifscgr  28471  trgcgrg  28478  motcgr3  28508  tgbtwnconn1lem1  28535  tgbtwnconn1lem2  28536  ismir  28622  miriso  28633  midexlem  28655  ragmir  28663  footexALT  28681  footexlem1  28682  footexlem2  28683  colperpexlem3  28695  mideulem2  28697  midex  28700  opphllem3  28712  midcgr  28743  lmiisolem  28759  brbtwn2  28868  colinearalglem4  28872  axsegconlem1  28880  axpaschlem  28903  axcontlem4  28930  axcontlem7  28933  axcontlem8  28934  ushgredgedgloop  29194  crctcshwlkn0lem6  29778  wwlknlsw  29810  wwlksnextwrd  29860  clwlkclwwlklem2a3  29956  clwlkclwwlk2  29965  clwwlkel  30008  clwwlkfo  30012  clwwlkext2edg  30018  eupth2eucrct  30179  numclwwlk2lem1lem  30304  numclwwlk1lem2fo  30320  numclwlk2lem2f  30339  grpoidinvlem2  30467  nvmtri  30633  cnnvm  30644  nvnd  30650  ipidsq  30672  ipnm  30673  ipipcj  30677  blocnilem  30766  ipasslem2  30794  dipsubdir  30810  hvaddsubval  30995  pjhthlem1  31353  pjspansn  31539  pjo  31633  unoplin  31882  adjadj  31898  hmoplin  31904  eigvec1  31924  lnopeqi  31970  nmcexi  31988  lnfnsubi  32008  riesz3i  32024  kbass6  32083  leoprf2  32089  leoprf  32090  pjnmopi  32110  mdslmd1lem1  32287  mdslmd1lem2  32288  superpos  32316  ifeq3da  32508  fgreu  32629  resf1o  32686  quad3d  32706  fprodex01  32783  sgnmul  32793  ccatws1f1o  32906  wrdt2ind  32908  mndlactfo  32994  mndractfo  32996  gsummpt2d  33015  xrge0tsmseq  33030  gsumwrd2dccatlem  33032  gsumwrd2dccat  33033  symgfcoeu  33037  wrdpmtrlast  33048  psgnfzto1stlem  33055  psgnfzto1st  33060  cycpm2tr  33074  cycpmco2lem6  33086  cycpmco2lem7  33087  subrgchr  33190  elrgspnlem1  33195  elrgspnlem3  33197  elrgspnsubrunlem1  33200  rloccring  33223  rhmdvd  33275  qusrn  33359  nsgqusf1olem3  33365  rhmquskerlem  33375  elrspunsn  33379  mxidlirredi  33421  qsdrngi  33445  1arithidomlem1  33485  1arithidomlem2  33486  evls1subd  33520  r1pid2OLD  33553  resssra  33562  dimval  33575  dimvalfi  33576  lindsunlem  33599  dimkerim  33602  qusdimsum  33603  fedgmullem1  33604  extdg1id  33640  fldextrspunlsplem  33647  fldextrspunlsp  33648  fldextrspunlem1  33649  fldextrspundgdvds  33655  ply1annidllem  33670  algextdeglem4  33689  constrrtcc  33704  constrsslem  33710  constrresqrtcl  33746  cos9thpiminplylem2  33752  cos9thpiminply  33757  madjusmdetlem2  33797  qtophaus  33805  zarclssn  33842  zarcmplem  33850  pstmval  33864  mndpluscn  33895  qqhucn  33961  esumval  34015  gsumesum  34028  esumcst  34032  esumpcvgval  34047  oddpwdc  34324  eulerpartlemgvv  34346  probdif  34390  signsvtn  34554  actfunsnf1o  34574  reprpmtf1o  34596  hgt750lemd  34618  logdivsqrle  34620  hgt750lemg  34624  hgt750lemb  34626  bnj1415  35007  swrdrevpfx  35092  pfxwlk  35099  derangen2  35149  subfaclefac  35151  subfaclim  35163  satom  35331  fmla  35356  mrsubrn  35488  sinccvglem  35647  bcprod  35713  filnetlem4  36357  curunc  37584  ltflcei  37590  matunitlindflem1  37598  matunitlindflem2  37599  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem24  37626  mblfinlem4  37642  ibladdnclem  37658  iblabsnc  37666  iblmulc2nc  37667  ftc1anclem6  37680  ftc1anclem8  37682  sdclem2  37724  ismtycnv  37784  heiborlem10  37802  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  42016  3lexlogpow5ineq5  42036  aks4d1p1  42052  primrootsunit1  42073  primrootscoprmpow  42075  posbezout  42076  aks6d1c1p3  42086  aks6d1c1p4  42087  aks6d1c1p5  42088  aks6d1c1p7  42089  evl1gprodd  42093  hashscontpow1  42097  aks6d1c3  42099  aks6d1c2lem3  42102  aks6d1c2lem4  42103  aks6d1c2  42106  aks6d1c5lem3  42113  aks6d1c6lem1  42146  aks6d1c6isolem3  42152  aks6d1c6lem5  42153  bcle2d  42155  aks6d1c7lem1  42156  aks5lem3a  42165  grpods  42170  unitscyglem1  42171  unitscyglem2  42172  unitscyglem4  42174  unitscyglem5  42175  aks5lem7  42176  nicomachus  42288  sumcubes  42289  cnreeu  42466  frlmvscadiccat  42482  grpcominv1  42484  riccrng1  42497  ricdrng1  42504  frlmsnic  42516  evlselv  42563  fsuppind  42566  flt4lem7  42635  negexpidd  42658  3cubeslem2  42661  3cubeslem3r  42663  mzpsubmpt  42719  irrapxlem3  42800  pellexlem6  42810  pell1234qrne0  42829  pell1234qrreccl  42830  pell1234qrmulcl  42831  pell14qrdich  42845  pell1qrgaplem  42849  rmxluc  42912  rmyluc  42913  jm2.24nn  42935  jm2.18  42964  jm2.19lem2  42966  jm2.19lem3  42967  jm2.22  42971  jm2.23  42972  jm2.16nn0  42980  jm2.27c  42983  fnwe2lem2  43027  lmhmfgsplit  43062  hbtlem2  43100  onsucf1lem  43245  ofoafo  43332  naddcnffo  43340  naddwordnexlem4  43377  reabssgn  43612  relexpmulnn  43685  relexpmulg  43686  ntrclsneine0lem  44040  int-addassocd  44150  dvconstbi  44310  bccm1k  44318  binomcxplemnotnn0  44332  fmptsnxp  45150  wessf1ornlem  45166  projf1o  45178  infnsuprnmpt  45231  lefldiveq  45277  lt4addmuld  45291  fzdifsuc2  45295  suplesup  45322  infrpge  45334  xrlexaddrp  45335  xralrple2  45337  infleinflem1  45353  supminfrnmpt  45428  supminfxr2  45452  fsumnncl  45557  limcperiod  45613  sumnnodd  45615  limcresiooub  45627  limcresioolb  45628  0ellimcdiv  45634  reclimc  45638  limsupval3  45677  limsupequzmpt2  45703  liminfval5  45750  limsupresxr  45751  liminfresxr  45752  liminfvalxr  45768  liminfequzmpt2  45776  climliminflimsupd  45786  liminfltlem  45789  liminflbuz2  45800  sinmulcos  45850  coskpi2  45851  cncfdmsn  45875  cncfiooicclem1  45878  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  fperdvper  45904  dvnmptdivc  45923  dvnxpaek  45927  dvnmul  45928  dvnprodlem1  45931  dvnprodlem3  45933  itgcoscmulx  45954  itgsincmulx  45959  itgspltprt  45964  itgiccshift  45965  itgperiod  45966  sublevolico  45969  volioof  45972  ovolsplit  45973  fvvolioof  45974  fvvolicof  45976  stoweidlem22  46007  stoweidlem32  46017  wallispilem5  46054  stirlinglem5  46063  dirkertrigeqlem2  46084  dirkertrigeq  46086  dirkercncflem1  46088  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem13  46105  fourierdlem16  46108  fourierdlem19  46111  fourierdlem21  46113  fourierdlem22  46114  fourierdlem28  46120  fourierdlem32  46124  fourierdlem33  46125  fourierdlem42  46134  fourierdlem47  46138  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem56  46147  fourierdlem60  46151  fourierdlem61  46152  fourierdlem64  46155  fourierdlem66  46157  fourierdlem71  46162  fourierdlem73  46164  fourierdlem74  46165  fourierdlem76  46167  fourierdlem78  46169  fourierdlem79  46170  fourierdlem80  46171  fourierdlem81  46172  fourierdlem83  46174  fourierdlem88  46179  fourierdlem92  46183  fourierdlem93  46184  fourierdlem97  46188  fourierdlem101  46192  fourierdlem103  46194  fourierdlem104  46195  fourierdlem109  46200  fourierdlem111  46202  fouriersw  46216  elaa2lem  46218  etransclem24  46243  etransclem25  46244  etransclem35  46254  etransclem46  46265  rrndistlt  46275  rrxunitopnfi  46277  qndenserrnbl  46280  qndenserrnopnlem  46282  saldifcl2  46313  intsal  46315  sge0sn  46364  sge0ltfirp  46385  sge0iunmptlemre  46400  sge0fodjrnlem  46401  sge0isum  46412  sge0xaddlem1  46418  nnfoctbdjlem  46440  meassle  46448  ismeannd  46452  meadif  46464  meaiuninclem  46465  meaiininclem  46471  omeunile  46490  caragendifcl  46499  caratheodory  46513  isomenndlem  46515  ovnsubaddlem1  46555  hoidmv1lelem2  46577  hoidmv1le  46579  hoidmvlelem2  46581  hoidmvle  46585  hoi2toco  46592  rrnmbl  46599  hoidifhspdmvle  46605  voncmpl  46606  hoiqssbl  46610  hspmbllem1  46611  hspmbllem2  46612  ovolval2lem  46628  ovolval5lem2  46638  ovnovollem1  46641  ovnovollem2  46642  hoimbl2  46650  vonhoire  46657  salpreimagelt  46692  salpreimalegt  46694  preimaioomnf  46704  smfres  46775  smfmullem1  46776  smflimmpt  46795  smfsupmpt  46800  smfinfmpt  46804  smflimsupmpt  46814  smfliminflem  46815  smfliminfmpt  46817  sigarcol  46849  f1oresf1o  47278  elsprel  47463  prproropf1o  47495  paireqne  47499  sfprmdvdsmersenne  47591  lighneallem3  47595  lighneallem4  47598  nn0onn0exALTV  47687  nnsum3primesprm  47778  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  isuspgrim0lem  47881  clnbgrgrimlem  47921  uspgrlimlem3  47978  uspgrlimlem4  47979  gpgedgvtx0  48049  gpgedgvtx1  48050  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