Theorem eqtr2d 2801

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  3eqtrrd  2805  3eqtr2rd  2807  ifan  4543  ifor  4544  dfopif  4837  fnco  6657  fnsnfv  6964  nvocnv  7288  elovmpt3rab1  7680  onsucmin  7823  csbopeq1a  8053  oaabs2  8641  ecinxp  8796  resixpfo  8940  sbthlem3  9084  rankxpsuc  9861  fseqenlem2  10025  dfac2b  10130  isf32lem9  10360  compsscnvlem  10369  ttukeylem7  10514  fpwwe2lem10  10640  00id  11400  submul2  11669  mulsubfacd  11690  divadddiv  11945  infrenegsup  12213  xadd4d  13345  fzdifsuc  13629  fzval3  13780  fzoshftral  13833  ceim1l  13898  fldiv  13911  flmod  13936  intfrac  13937  modcyc2  13958  modaddb  13960  moddi  13993  uzrdgfni  14012  axdc4uzlem  14037  seqf1olem1  14095  seqf1olem2  14096  seqid2  14102  expnegz  14150  binom2sub  14274  binom3  14278  hashreshashfun  14494  ccatw2s1p2  14695  ccats1pfxeq  14773  pfxccatin12lem2  14790  pfxccatin12  14792  swrdccat3b  14799  swrdrevpfx  14828  cshweqrep  14882  2cshwcshw  14886  ccatco  14896  swrds2  15001  relexpsucnnr  15086  relexpaddnn  15112  sgnmul  15168  reim  15184  mulre  15196  addcj  15223  absimle  15384  clim2ser  15730  isercoll2  15744  serf0  15756  iseralt  15760  summolem3  15788  isumclim3  15833  mptfzshft  15852  fsumrev  15853  fsum2mul  15863  incexc  15914  isumsplit  15917  mertenslem1  15961  fprodrev  16054  iprodclim3  16077  binomfallfaclem2  16116  ef4p  16191  tanval3  16212  efival  16230  sinmul  16250  bitsinvp1  16529  sadaddlem  16546  bitsshft  16555  smu01lem  16565  dfgcd2  16626  lcmgcdlem  16686  lcm1  16690  lcmfass  16726  eulerthlem2  16863  hashgcdeq  16871  powm2modprm  16885  pythagtriplem16  16912  pczpre  16929  pcqdiv  16939  pcadd  16971  pcfac  16981  prmreclem5  17002  4sqlem10  17029  4sqlem19  17045  vdwapun  17056  vdwlem1  17063  ramcl  17111  setsstruct  17258  strfvd  17282  strfv2d  17283  xpsff1o  17643  xpsrnbas  17647  2oppccomf  17803  oppcepi  17818  sscfn1  17896  sscfn2  17897  invfuc  18056  funcestrcsetclem7  18224  funcsetcestrclem7  18239  gsumsplit1r  18777  grpinvssd  19127  grpinvval2  19133  cycsubggend  19320  pmtrdifwrdellem2  19596  psgnunilem1  19607  psgnuni  19613  pgp0  19710  sylow1lem1  19712  sylow3lem2  19742  efgredleme  19857  efgcpbllemb  19869  frgpuptinv  19885  frgpup3lem  19891  gexexlem  19966  cyggenod  19998  gsumval3eu  20018  gsumval3  20021  gsumzaddlem  20035  dprd2db  20159  ablsimpgfindlem1  20223  ringinvdv  20542  c0snmgmhm  20590  rngcifuestrc  20788  funcrngcsetc  20789  funcrngcsetcALT  20790  funcringcsetc  20823  lss1d  21134  pwssplit1  21230  rhmqusnsg  21475  rngqiprnglin  21492  znzrh2  21745  regsumsupp  21822  ipassr2  21847  dsmmfi  21938  frlmlss  21951  frlmip  21978  frlmlbs  21997  frlmup3  22000  islindf4  22038  mplcoe3  22239  subrgascl  22267  evlseu  22284  psdadd  22376  ply1sclid  22499  ply1chr  22516  evls1addd  22581  evls1muld  22582  evls1vsca  22583  evls1maprhm  22586  evls1maplmhm  22587  evls1maprnss  22588  evl1maprhm  22589  1marepvmarrepid  22782  madurid  22851  smadiadetlem3  22875  mat2pmatghm  22937  pmatcollpwscmatlem1  22996  pm2mpmhmlem2  23026  cpmadurid  23074  cpmidgsumm2pm  23076  cpmadugsumlemB  23081  cayhamlem2  23091  ntrval2  23258  ordtuni  23397  cnclima  23475  cmpsub  23607  ptbasfi  23789  txbasval  23814  pt1hmeo  24014  alexsubALTlem1  24255  trust  24437  ussid  24468  ressuss  24470  ressprdsds  24579  imasdsf1olem  24581  setsms  24688  tmsxms  24694  tmsxpsmopn  24745  subgnm  24841  tngnm  24859  tngngp2  24860  xrsxmet  25018  xrge0gsumle  25042  metdstri  25060  xrhmeo  25156  lebnumlem3  25173  pcorevlem  25236  pi1xfrcnvlem  25266  clmabs  25293  cvsmuleqdivd  25344  rrxip  25600  rrxds  25603  rrxdsfi  25621  minveclem4a  25640  pjthlem1  25647  divcncf  25657  ovolunlem1a  25706  mbfres2  25855  i1faddlem  25903  ibladdlem  26030  iblabs  26039  ditgsplit  26071  dvmptresicc  26126  dvnres  26141  dvmptdiv  26184  dveflem  26189  dveq0  26210  dvfsumabs  26233  itgsubstlem  26258  ply1divex  26345  r1pid2  26370  dgrco  26483  plycjlem  26484  taylthlem1  26587  pserdv2  26644  abelthlem6  26650  abelthlem7  26652  tangtx  26721  abssinper  26737  sineq0  26740  explog  26810  reexplog  26811  eflogeq  26818  abslogle  26834  tanarg  26835  logtayl  26876  logtayl2  26878  relogbdiv  26995  ang180lem3  27027  affineequiv  27039  affineequiv2  27040  chordthmlem4  27051  chordthmlem5  27052  heron  27054  dcubic1lem  27059  dcubic2  27060  dcubic  27062  mcubic  27063  cubic2  27064  dquartlem1  27067  dquart  27069  quart1lem  27071  quartlem1  27073  quart  27077  acoscos  27109  atanlogaddlem  27129  atantayl2  27154  atantayl3  27155  birthdaylem2  27168  efrlim  27185  amgmlem  27205  logdifbnd  27209  emcllem3  27213  emcllem6  27216  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamgulmlem4  27247  lgamgulmlem5  27248  gamigam  27268  lgamcvg2  27270  gamfac  27282  basellem3  27298  basellem8  27303  basellem9  27304  chtprm  27368  logfaclbnd  27437  perfect1  27443  bcp1ctr  27494  bclbnd  27495  bposlem1  27499  lgsdilem  27539  lgsdirnn0  27559  lgsdinn0  27560  gausslemma2dlem1a  27580  gausslemma2dlem4  27584  gausslemma2dlem5a  27585  lgseisenlem2  27591  lgsquadlem1  27595  2sqlem2  27633  mul2sq  27634  2sqmod  27651  2sqnn0  27653  vmadivsum  27697  rpvmasumlem  27702  dchrisumlem1  27704  dchrisumlem2  27705  dchrmusum2  27709  dchrvmasum2if  27712  dchrisum0lem2  27733  logsqvma2  27758  selberg3  27774  selberg4lem1  27775  pntrsumo1  27780  pntrlog2bndlem2  27793  pntrlog2bndlem3  27794  pntrlog2bndlem5  27796  pntibndlem2  27806  pntlemk  27821  pntlemo  27822  ostth2lem4  27851  ostth3  27853  subsfo  28309  negsval2  28310  ltonold  28505  noseqrdgfn  28550  n0fincut  28599  addhalfcut  28703  bdayfinbndlem1  28711  z12shalf  28724  tgbtwndiff  28826  tgifscgr  28828  trgcgrg  28835  motcgr3  28865  tgbtwnconn1lem1  28892  tgbtwnconn1lem2  28893  ismir  28987  miriso  28998  midexlem  29020  symquadprlnglem  29021  ragmir  29031  footexALT  29049  footexlem1  29050  footexlem2  29051  colperpexlem3  29064  mideulem2  29066  midex  29069  opphllem3  29081  midcgr  29140  lmiisolem  29156  prlngmid2  29266  quadcgrprlng  29271  brbtwn2  29310  colinearalglem4  29314  axsegconlem1  29322  axpaschlem  29345  axcontlem4  29372  axcontlem7  29375  axcontlem8  29376  ushgredgedgloop  29639  pfxwlk  30093  crctcshwlkn0lem6  30231  wwlknlsw  30263  wwlksnextwrd  30313  clwlkclwwlklem2a3  30412  clwlkclwwlk2  30421  clwwlkel  30464  clwwlkfo  30468  clwwlkext2edg  30474  eupth2eucrct  30639  numclwwlk2lem1lem  30764  numclwwlk1lem2fo  30780  numclwlk2lem2f  30799  grpoidinvlem2  30928  nvmtri  31094  cnnvm  31105  nvnd  31111  ipidsq  31133  ipnm  31134  ipipcj  31138  blocnilem  31227  ipasslem2  31255  dipsubdir  31271  hvaddsubval  31456  pjhthlem1  31814  pjspansn  32000  pjo  32094  unoplin  32343  adjadj  32359  hmoplin  32365  eigvec1  32385  lnopeqi  32431  nmcexi  32449  lnfnsubi  32469  riesz3i  32485  kbass6  32544  leoprf2  32550  leoprf  32551  pjnmopi  32571  mdslmd1lem1  32748  mdslmd1lem2  32749  superpos  32777  ifeq3da  32963  fgreu  33087  cocnvf1o  33144  resf1o  33145  quad3d  33164  fprodex01  33239  ccatws1f1o  33337  wrdt2ind  33339  mndlactfo  33411  mndractfo  33413  gsummpt2d  33433  gsummptp1  33441  xrge0tsmseq  33459  gsumwrd2dccatlem  33461  gsumwrd2dccat  33462  symgfcoeu  33466  wrdpmtrlast  33477  psgnfzto1stlem  33484  psgnfzto1st  33489  cycpm2tr  33503  cycpmco2lem6  33515  cycpmco2lem7  33516  subrgchr  33620  elrgspnlem1  33626  elrgspnlem3  33628  elrgspnsubrunlem1  33631  rloccring  33655  rhmdvd  33708  qusrn  33782  nsgqusf1olem3  33788  rhmquskerlem  33797  elrspunsn  33801  mxidlirredi  33818  qsdrngi  33841  1arithidomlem1  33889  1arithidomlem2  33890  evls1subd  33926  deg1prod  33937  0mplrim  33968  evlextv  33996  psrmonprod  34006  esplyfval1  34027  esplyind  34029  esplyindfv  34030  esplyfvn  34031  vietalem  34033  resssra  34041  dimval  34055  dimvalfi  34056  lindsunlem  34078  dimkerim  34081  qusdimsum  34082  fedgmullem1  34083  extdg1id  34120  fldextrspunlsplem  34127  fldextrspunlsp  34128  fldextrspunlem1  34129  fldextrspundgdvds  34135  extdgfialglem1  34146  extdgfialglem2  34147  ply1annidllem  34155  algextdeglem4  34174  constrrtcc  34189  constrsslem  34195  constrresqrtcl  34231  cos9thpiminplylem2  34237  cos9thpiminply  34242  madjusmdetlem2  34282  qtophaus  34290  zarclssn  34327  zarcmplem  34335  pstmval  34349  mndpluscn  34380  qqhucn  34446  esumval  34500  gsumesum  34513  esumcst  34517  esumpcvgval  34532  oddpwdc  34809  eulerpartlemgvv  34831  probdif  34875  signsvtn  35036  actfunsnf1o  35056  reprpmtf1o  35078  hgt750lemd  35100  logdivsqrle  35102  hgt750lemg  35106  hgt750lemb  35108  bnj1415  35491  vonf1oonfo  35656  derangen2  35703  subfaclefac  35705  subfaclim  35717  satom  35885  fmla  35910  mrsubrn  36042  sinccvglem  36201  bcprod  36267  nmulss1  36743  filnetlem4  36949  curunc  38310  ltflcei  38316  matunitlindflem1  38324  matunitlindflem2  38325  poimirlem16  38344  poimirlem17  38345  poimirlem19  38347  poimirlem20  38348  poimirlem24  38352  mblfinlem4  38368  ibladdnclem  38384  iblabsnc  38392  iblmulc2nc  38393  ftc1anclem6  38406  ftc1anclem8  38408  sdclem2  38451  ismtycnv  38511  heiborlem10  38529  lflvsass  39913  lkrscss  39930  eqlkr  39931  eqlkr3  39933  ldualvsdi2  39976  omllaw3  40077  cmtcomlemN  40080  cmtbr3N  40086  omlfh3N  40091  llnexchb2lem  40700  dalawlem7  40709  dalawlem11  40713  dalawlem12  40714  pol1N  40742  paddatclN  40781  4atexlemcnd  40904  ltrncoidN  40960  cdleme3b  41061  cdleme11  41102  cdleme15a  41106  cdleme22e  41176  cdleme22g  41180  cdlemg18b  41511  trlcoat  41555  cdlemk2  41664  cdlemk4  41666  cdlemki  41673  cdlemksv2  41679  cdlemk15  41687  cdlemk55a  41791  diainN  41889  dia2dimlem3  41898  dia2dimlem5  41900  dvhlveclem  41940  diaocN  41957  cdlemn4  42030  cdlemn8  42036  dihopelvalcpre  42080  dihmeetlem9N  42147  dih1dimatlem  42161  dihpN  42168  dochvalr3  42195  dochsat  42215  djhjlj  42235  dochdmm1  42242  dihjatcclem4  42253  dihjat1  42261  dihjat4  42265  dochsnkr2cl  42306  dochfl1  42308  lclkrlem2j  42348  mapdordlem2  42469  mapdrvallem2  42477  hdmap10  42672  lcmineqlem12  42865  3lexlogpow5ineq5  42885  aks4d1p1  42901  primrootsunit1  42922  primrootscoprmpow  42924  posbezout  42925  aks6d1c1p3  42935  aks6d1c1p4  42936  aks6d1c1p5  42937  aks6d1c1p7  42938  evl1gprodd  42942  hashscontpow1  42946  aks6d1c3  42948  aks6d1c2lem3  42951  aks6d1c2lem4  42952  aks6d1c2  42955  aks6d1c5lem3  42962  aks6d1c6lem1  42995  aks6d1c6isolem3  43001  aks6d1c6lem5  43002  bcle2d  43004  aks6d1c7lem1  43005  aks5lem3a  43014  grpods  43019  unitscyglem1  43020  unitscyglem2  43021  unitscyglem4  43023  unitscyglem5  43024  aks5lem7  43025  nicomachus  43131  sumcubes  43132  cnreeu  43322  frlmvscadiccat  43338  grpcominv1  43340  riccrng1  43347  ricdrng1  43354  frlmsnic  43366  evlselv  43379  fsuppind  43380  flt4lem7  43449  negexpidd  43471  3cubeslem2  43474  3cubeslem3r  43476  mzpsubmpt  43532  irrapxlem3  43609  pellexlem6  43619  pell1234qrne0  43638  pell1234qrreccl  43639  pell1234qrmulcl  43640  pell14qrdich  43654  pell1qrgaplem  43658  rmxluc  43721  rmyluc  43722  jm2.24nn  43744  jm2.18  43773  jm2.19lem2  43775  jm2.19lem3  43776  jm2.22  43780  jm2.23  43781  jm2.16nn0  43789  jm2.27c  43792  fnwe2lem2  43836  lmhmfgsplit  43871  hbtlem2  43909  onsucf1lem  44054  ofoafo  44141  naddcnffo  44149  naddwordnexlem4  44186  reabssgn  44420  relexpmulnn  44493  relexpmulg  44494  ntrclsneine0lem  44848  int-addassocd  44958  dvconstbi  45102  bccm1k  45110  binomcxplemnotnn0  45124  fmptsnxp  45945  wessf1ornlem  45961  projf1o  45972  infnsuprnmpt  46023  lefldiveq  46069  lt4addmuld  46083  fzdifsuc2  46087  suplesup  46113  infrpge  46125  xrlexaddrp  46126  xralrple2  46128  infleinflem1  46143  supminfrnmpt  46217  supminfxr2  46241  fsumnncl  46346  limcperiod  46402  sumnnodd  46404  limcresiooub  46414  limcresioolb  46415  0ellimcdiv  46421  reclimc  46425  limsupval3  46464  limsupequzmpt2  46490  liminfval5  46537  limsupresxr  46538  liminfresxr  46539  liminfvalxr  46555  liminfequzmpt2  46563  climliminflimsupd  46573  liminfltlem  46576  liminflbuz2  46587  sinmulcos  46637  coskpi2  46638  cncfdmsn  46662  cncfiooicclem1  46665  fprodsubrecnncnvlem  46679  fprodaddrecnncnvlem  46681  fperdvper  46691  dvnmptdivc  46710  dvnxpaek  46714  dvnmul  46715  dvnprodlem1  46718  dvnprodlem3  46720  itgcoscmulx  46741  itgsincmulx  46746  itgspltprt  46751  itgiccshift  46752  itgperiod  46753  sublevolico  46756  volioof  46759  ovolsplit  46760  fvvolioof  46761  fvvolicof  46763  stoweidlem22  46794  stoweidlem32  46804  wallispilem5  46841  stirlinglem5  46850  dirkertrigeqlem2  46871  dirkertrigeq  46873  dirkercncflem1  46875  dirkercncflem2  46876  dirkercncflem4  46878  fourierdlem13  46892  fourierdlem16  46895  fourierdlem19  46898  fourierdlem21  46900  fourierdlem22  46901  fourierdlem28  46907  fourierdlem32  46911  fourierdlem33  46912  fourierdlem42  46921  fourierdlem47  46925  fourierdlem48  46926  fourierdlem49  46927  fourierdlem50  46928  fourierdlem56  46934  fourierdlem60  46938  fourierdlem61  46939  fourierdlem64  46942  fourierdlem66  46944  fourierdlem71  46949  fourierdlem73  46951  fourierdlem74  46952  fourierdlem76  46954  fourierdlem78  46956  fourierdlem79  46957  fourierdlem80  46958  fourierdlem81  46959  fourierdlem83  46961  fourierdlem88  46966  fourierdlem92  46970  fourierdlem93  46971  fourierdlem97  46975  fourierdlem101  46979  fourierdlem103  46981  fourierdlem104  46982  fourierdlem109  46987  fourierdlem111  46989  fouriersw  47003  elaa2lem  47005  etransclem24  47030  etransclem25  47031  etransclem35  47041  etransclem46  47052  rrndistlt  47062  rrxunitopnfi  47064  qndenserrnbl  47067  qndenserrnopnlem  47069  saldifcl2  47100  intsal  47102  sge0sn  47151  sge0ltfirp  47172  sge0iunmptlemre  47187  sge0fodjrnlem  47188  sge0isum  47199  sge0xaddlem1  47205  nnfoctbdjlem  47227  meassle  47235  ismeannd  47239  meadif  47251  meaiuninclem  47252  meaiininclem  47258  omeunile  47277  caragendifcl  47286  caratheodory  47300  isomenndlem  47302  ovnsubaddlem1  47342  hoidmv1lelem2  47364  hoidmv1le  47366  hoidmvlelem2  47368  hoidmvle  47372  hoi2toco  47379  rrnmbl  47386  hoidifhspdmvle  47392  voncmpl  47393  hoiqssbl  47397  hspmbllem1  47398  hspmbllem2  47399  ovolval2lem  47415  ovolval5lem2  47425  ovnovollem1  47428  ovnovollem2  47429  hoimbl2  47437  vonhoire  47444  salpreimagelt  47479  salpreimalegt  47481  preimaioomnf  47491  smfres  47562  smfmullem1  47563  smflimmpt  47582  smfsupmpt  47587  smfinfmpt  47591  smflimsupmpt  47601  smfliminflem  47602  smfliminfmpt  47604  sigarcol  47636  sin5tlem2  47669  f1oresf1o  48085  elsprel  48282  prproropf1o  48314  paireqne  48318  sfprmdvdsmersenne  48413  lighneallem3  48417  lighneallem4  48420  nprmdvdsfacm1lem1  48430  nn0onn0exALTV  48522  nnsum3primesprm  48613  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  isuspgrim0lem  48716  clnbgrgrimlem  48756  uspgrlimlem3  48813  uspgrlimlem4  48814  gpgedgvtx0  48884  gpgedgvtx1  48885  funcringcsetcALTV2lem7  49118  funcringcsetclem7ALTV  49141  lincext3  49293  lincresunit3  49318  nn0onn0ex  49360  nnpw2pmod  49420  blennn0em1  49428  digexp  49444  dignn0ehalf  49454  nn0mulfsum  49461  itcovalpclem1  49507  eenglngeehlnmlem2  49575  rrx2vlinest  49578  line2  49589  itschlc0xyqsol  49604  itsclinecirc0b  49611  toplatjoin  49837  toplatmeet  49838  upeu2lem  49863  oppff1o  49984  imaf1co  49990  upciclem3  50003  natoppfb  50066  oppcthinco  50274  oppcthinendcALT  50276  lmddu  50502  recsec  50591  reccsc  50592  aacllem  50678  crossp3d  50706  amgmlemALT  50708