Theorem eqtr2d 2797

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

Syntax hints:   → wi 4   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  3eqtrrd  2801  3eqtr2rd  2803  ifan  4531  ifor  4532  dfopif  4825  fnco  6634  fnsnfv  6941  nvocnv  7260  elovmpt3rab1  7651  onsucmin  7796  csbopeq1a  8026  oaabs2  8613  ecinxp  8768  resixpfo  8912  sbthlem3  9055  rankxpsuc  9834  fseqenlem2  9975  dfac2b  10081  isf32lem9  10312  compsscnvlem  10321  ttukeylem7  10466  fpwwe2lem10  10592  00id  11352  submul2  11621  mulsubfacd  11642  divadddiv  11900  infrenegsup  12169  xadd4d  13300  fzdifsuc  13583  fzval3  13734  fzoshftral  13787  ceim1l  13851  fldiv  13864  flmod  13889  intfrac  13890  modcyc2  13911  modaddb  13913  moddi  13946  uzrdgfni  13965  axdc4uzlem  13990  seqf1olem1  14048  seqf1olem2  14049  seqid2  14055  expnegz  14103  binom2sub  14227  binom3  14231  hashreshashfun  14446  ccatw2s1p2  14645  ccats1pfxeq  14721  pfxccatin12lem2  14738  pfxccatin12  14740  swrdccat3b  14747  cshweqrep  14828  2cshwcshw  14832  ccatco  14842  swrds2  14947  relexpsucnnr  15032  relexpaddnn  15058  sgnmul  15111  reim  15127  mulre  15139  addcj  15166  absimle  15327  clim2ser  15673  isercoll2  15687  serf0  15699  iseralt  15703  summolem3  15732  isumclim3  15777  mptfzshft  15796  fsumrev  15797  fsum2mul  15807  incexc  15858  isumsplit  15861  mertenslem1  15905  fprodrev  15998  iprodclim3  16021  binomfallfaclem2  16061  ef4p  16136  tanval3  16157  efival  16175  sinmul  16195  bitsinvp1  16474  sadaddlem  16491  bitsshft  16500  smu01lem  16510  dfgcd2  16571  lcmgcdlem  16631  lcm1  16635  lcmfass  16671  eulerthlem2  16808  hashgcdeq  16816  powm2modprm  16830  pythagtriplem16  16857  pczpre  16874  pcqdiv  16884  pcadd  16916  pcfac  16926  prmreclem5  16947  4sqlem10  16974  4sqlem19  16990  vdwapun  17001  vdwlem1  17008  ramcl  17056  setsstruct  17203  strfvd  17227  strfv2d  17228  xpsff1o  17588  xpsrnbas  17592  2oppccomf  17748  oppcepi  17763  sscfn1  17841  sscfn2  17842  invfuc  18001  funcestrcsetclem7  18169  funcsetcestrclem7  18184  gsumsplit1r  18712  grpinvssd  19050  grpinvval2  19056  cycsubggend  19237  pmtrdifwrdellem2  19513  psgnunilem1  19524  psgnuni  19530  pgp0  19627  sylow1lem1  19629  sylow3lem2  19659  efgredleme  19774  efgcpbllemb  19786  frgpuptinv  19802  frgpup3lem  19808  gexexlem  19883  cyggenod  19915  gsumval3eu  19935  gsumval3  19938  gsumzaddlem  19952  dprd2db  20076  ablsimpgfindlem1  20140  ringinvdv  20450  c0snmgmhm  20498  rngcifuestrc  20676  funcrngcsetc  20677  funcrngcsetcALT  20678  funcringcsetc  20711  lss1d  21018  pwssplit1  21114  rhmqusnsg  21343  rngqiprnglin  21360  znzrh2  21585  regsumsupp  21662  ipassr2  21687  dsmmfi  21778  frlmlss  21791  frlmip  21818  frlmlbs  21837  frlmup3  21840  islindf4  21878  mplcoe3  22079  subrgascl  22107  evlseu  22124  psdadd  22216  ply1sclid  22339  ply1chr  22357  evls1addd  22422  evls1muld  22423  evls1vsca  22424  evls1maprhm  22427  evls1maplmhm  22428  evls1maprnss  22429  evl1maprhm  22430  1marepvmarrepid  22623  madurid  22692  smadiadetlem3  22716  mat2pmatghm  22778  pmatcollpwscmatlem1  22837  pm2mpmhmlem2  22867  cpmadurid  22915  cpmidgsumm2pm  22917  cpmadugsumlemB  22922  cayhamlem2  22932  ntrval2  23099  ordtuni  23238  cnclima  23316  cmpsub  23448  ptbasfi  23629  txbasval  23654  pt1hmeo  23854  alexsubALTlem1  24095  trust  24277  ussid  24308  ressuss  24310  ressprdsds  24419  imasdsf1olem  24421  setsms  24528  tmsxms  24534  tmsxpsmopn  24585  subgnm  24681  tngnm  24699  tngngp2  24700  xrsxmet  24858  xrge0gsumle  24882  metdstri  24900  xrhmeo  24996  lebnumlem3  25013  pcorevlem  25076  pi1xfrcnvlem  25106  clmabs  25133  cvsmuleqdivd  25184  rrxip  25440  rrxds  25443  rrxdsfi  25461  minveclem4a  25480  pjthlem1  25487  divcncf  25497  ovolunlem1a  25546  mbfres2  25695  i1faddlem  25743  ibladdlem  25870  iblabs  25879  ditgsplit  25911  dvmptresicc  25966  dvnres  25981  dvmptdiv  26024  dveflem  26029  dveq0  26050  dvfsumabs  26073  itgsubstlem  26098  ply1divex  26185  r1pid2  26210  dgrco  26323  plycjlem  26324  taylthlem1  26424  pserdv2  26481  abelthlem6  26487  abelthlem7  26489  tangtx  26558  abssinper  26574  sineq0  26577  explog  26647  reexplog  26648  eflogeq  26655  abslogle  26671  tanarg  26672  logtayl  26713  logtayl2  26715  relogbdiv  26832  ang180lem3  26864  affineequiv  26876  affineequiv2  26877  chordthmlem4  26888  chordthmlem5  26889  heron  26891  dcubic1lem  26896  dcubic2  26897  dcubic  26899  mcubic  26900  cubic2  26901  dquartlem1  26904  dquart  26906  quart1lem  26908  quartlem1  26910  quart  26914  acoscos  26946  atanlogaddlem  26966  atantayl2  26991  atantayl3  26992  birthdaylem2  27005  efrlim  27022  amgmlem  27042  logdifbnd  27046  emcllem3  27050  emcllem6  27053  lgamgulmlem2  27082  lgamgulmlem3  27083  lgamgulmlem4  27084  lgamgulmlem5  27085  gamigam  27105  lgamcvg2  27107  gamfac  27119  basellem3  27135  basellem8  27140  basellem9  27141  chtprm  27205  logfaclbnd  27274  perfect1  27280  bcp1ctr  27331  bclbnd  27332  bposlem1  27336  lgsdilem  27376  lgsdirnn0  27396  lgsdinn0  27397  gausslemma2dlem1a  27417  gausslemma2dlem4  27421  gausslemma2dlem5a  27422  lgseisenlem2  27428  lgsquadlem1  27432  2sqlem2  27470  mul2sq  27471  2sqmod  27488  2sqnn0  27490  vmadivsum  27534  rpvmasumlem  27539  dchrisumlem1  27541  dchrisumlem2  27542  dchrmusum2  27546  dchrvmasum2if  27549  dchrisum0lem2  27570  logsqvma2  27595  selberg3  27611  selberg4lem1  27612  pntrsumo1  27617  pntrlog2bndlem2  27630  pntrlog2bndlem3  27631  pntrlog2bndlem5  27633  pntibndlem2  27643  pntlemk  27658  pntlemo  27659  ostth2lem4  27688  ostth3  27690  subsfo  28146  negsval2  28147  ltonold  28342  noseqrdgfn  28387  n0fincut  28436  addhalfcut  28540  bdayfinbndlem1  28548  z12shalf  28561  tgbtwndiff  28663  tgifscgr  28665  trgcgrg  28672  motcgr3  28702  tgbtwnconn1lem1  28729  tgbtwnconn1lem2  28730  ismir  28816  miriso  28827  midexlem  28849  ragmir  28857  footexALT  28875  footexlem1  28876  footexlem2  28877  colperpexlem3  28889  mideulem2  28891  midex  28894  opphllem3  28906  midcgr  28937  lmiisolem  28953  brbtwn2  29063  colinearalglem4  29067  axsegconlem1  29075  axpaschlem  29098  axcontlem4  29125  axcontlem7  29128  axcontlem8  29129  ushgredgedgloop  29389  crctcshwlkn0lem6  29972  wwlknlsw  30004  wwlksnextwrd  30054  clwlkclwwlklem2a3  30153  clwlkclwwlk2  30162  clwwlkel  30205  clwwlkfo  30209  clwwlkext2edg  30215  eupth2eucrct  30376  numclwwlk2lem1lem  30501  numclwwlk1lem2fo  30517  numclwlk2lem2f  30536  grpoidinvlem2  30665  nvmtri  30831  cnnvm  30842  nvnd  30848  ipidsq  30870  ipnm  30871  ipipcj  30875  blocnilem  30964  ipasslem2  30992  dipsubdir  31008  hvaddsubval  31193  pjhthlem1  31551  pjspansn  31737  pjo  31831  unoplin  32080  adjadj  32096  hmoplin  32102  eigvec1  32122  lnopeqi  32168  nmcexi  32186  lnfnsubi  32206  riesz3i  32222  kbass6  32281  leoprf2  32287  leoprf  32288  pjnmopi  32308  mdslmd1lem1  32485  mdslmd1lem2  32486  superpos  32514  ifeq3da  32705  fgreu  32834  cocnvf1o  32892  resf1o  32893  quad3d  32912  fprodex01  32988  ccatws1f1o  33090  wrdt2ind  33092  mndlactfo  33166  mndractfo  33168  gsummpt2d  33190  gsummptp1  33198  xrge0tsmseq  33216  gsumwrd2dccatlem  33218  gsumwrd2dccat  33219  symgfcoeu  33223  wrdpmtrlast  33234  psgnfzto1stlem  33241  psgnfzto1st  33246  cycpm2tr  33260  cycpmco2lem6  33272  cycpmco2lem7  33273  subrgchr  33378  elrgspnlem1  33384  elrgspnlem3  33386  elrgspnsubrunlem1  33389  rloccring  33413  rhmdvd  33471  qusrn  33556  nsgqusf1olem3  33562  rhmquskerlem  33572  elrspunsn  33576  mxidlirredi  33620  qsdrngi  33644  1arithidomlem1  33692  1arithidomlem2  33693  evls1subd  33729  deg1prod  33740  r1pid2OLD  33766  0mplrim  33772  evlextv  33800  psrmonprod  33810  esplyfval1  33831  esplyind  33833  esplyindfv  33834  esplyfvn  33835  vietalem  33837  resssra  33845  dimval  33859  dimvalfi  33860  lindsunlem  33882  dimkerim  33885  qusdimsum  33886  fedgmullem1  33887  extdg1id  33924  fldextrspunlsplem  33931  fldextrspunlsp  33932  fldextrspunlem1  33933  fldextrspundgdvds  33939  extdgfialglem1  33950  extdgfialglem2  33951  ply1annidllem  33959  algextdeglem4  33978  constrrtcc  33993  constrsslem  33999  constrresqrtcl  34035  cos9thpiminplylem2  34041  cos9thpiminply  34046  madjusmdetlem2  34086  qtophaus  34094  zarclssn  34131  zarcmplem  34139  pstmval  34153  mndpluscn  34184  qqhucn  34250  esumval  34304  gsumesum  34317  esumcst  34321  esumpcvgval  34336  oddpwdc  34612  eulerpartlemgvv  34634  probdif  34678  signsvtn  34839  actfunsnf1o  34859  reprpmtf1o  34881  hgt750lemd  34903  logdivsqrle  34905  hgt750lemg  34909  hgt750lemb  34911  bnj1415  35294  vonf1oonfo  35419  swrdrevpfx  35428  pfxwlk  35435  derangen2  35485  subfaclefac  35487  subfaclim  35499  satom  35667  fmla  35692  mrsubrn  35824  sinccvglem  35983  bcprod  36049  filnetlem4  36702  curunc  38062  ltflcei  38068  matunitlindflem1  38076  matunitlindflem2  38077  poimirlem16  38096  poimirlem17  38097  poimirlem19  38099  poimirlem20  38100  poimirlem24  38104  mblfinlem4  38120  ibladdnclem  38136  iblabsnc  38144  iblmulc2nc  38145  ftc1anclem6  38158  ftc1anclem8  38160  sdclem2  38202  ismtycnv  38262  heiborlem10  38280  lflvsass  39666  lkrscss  39683  eqlkr  39684  eqlkr3  39686  ldualvsdi2  39729  omllaw3  39830  cmtcomlemN  39833  cmtbr3N  39839  omlfh3N  39844  llnexchb2lem  40453  dalawlem7  40462  dalawlem11  40466  dalawlem12  40467  pol1N  40495  paddatclN  40534  4atexlemcnd  40657  ltrncoidN  40713  cdleme3b  40814  cdleme11  40855  cdleme15a  40859  cdleme22e  40929  cdleme22g  40933  cdlemg18b  41264  trlcoat  41308  cdlemk2  41417  cdlemk4  41419  cdlemki  41426  cdlemksv2  41432  cdlemk15  41440  cdlemk55a  41544  diainN  41642  dia2dimlem3  41651  dia2dimlem5  41653  dvhlveclem  41693  diaocN  41710  cdlemn4  41783  cdlemn8  41789  dihopelvalcpre  41833  dihmeetlem9N  41900  dih1dimatlem  41914  dihpN  41921  dochvalr3  41948  dochsat  41968  djhjlj  41988  dochdmm1  41995  dihjatcclem4  42006  dihjat1  42014  dihjat4  42018  dochsnkr2cl  42059  dochfl1  42061  lclkrlem2j  42101  mapdordlem2  42222  mapdrvallem2  42230  hdmap10  42425  lcmineqlem12  42618  3lexlogpow5ineq5  42638  aks4d1p1  42654  primrootsunit1  42675  primrootscoprmpow  42677  posbezout  42678  aks6d1c1p3  42688  aks6d1c1p4  42689  aks6d1c1p5  42690  aks6d1c1p7  42691  evl1gprodd  42695  hashscontpow1  42699  aks6d1c3  42701  aks6d1c2lem3  42704  aks6d1c2lem4  42705  aks6d1c2  42708  aks6d1c5lem3  42715  aks6d1c6lem1  42748  aks6d1c6isolem3  42754  aks6d1c6lem5  42755  bcle2d  42757  aks6d1c7lem1  42758  aks5lem3a  42767  grpods  42772  unitscyglem1  42773  unitscyglem2  42774  unitscyglem4  42776  unitscyglem5  42777  aks5lem7  42778  nicomachus  42882  sumcubes  42883  cnreeu  43073  frlmvscadiccat  43089  grpcominv1  43091  riccrng1  43100  ricdrng1  43107  frlmsnic  43119  evlselv  43132  fsuppind  43133  flt4lem7  43202  negexpidd  43224  3cubeslem2  43227  3cubeslem3r  43229  mzpsubmpt  43285  irrapxlem3  43362  pellexlem6  43372  pell1234qrne0  43391  pell1234qrreccl  43392  pell1234qrmulcl  43393  pell14qrdich  43407  pell1qrgaplem  43411  rmxluc  43474  rmyluc  43475  jm2.24nn  43497  jm2.18  43526  jm2.19lem2  43528  jm2.19lem3  43529  jm2.22  43533  jm2.23  43534  jm2.16nn0  43542  jm2.27c  43545  fnwe2lem2  43589  lmhmfgsplit  43624  hbtlem2  43662  onsucf1lem  43807  ofoafo  43894  naddcnffo  43902  naddwordnexlem4  43939  reabssgn  44173  relexpmulnn  44246  relexpmulg  44247  ntrclsneine0lem  44601  int-addassocd  44711  dvconstbi  44871  bccm1k  44879  binomcxplemnotnn0  44893  fmptsnxp  45708  wessf1ornlem  45724  projf1o  45735  infnsuprnmpt  45786  lefldiveq  45832  lt4addmuld  45846  fzdifsuc2  45850  suplesup  45876  infrpge  45888  xrlexaddrp  45889  xralrple2  45891  infleinflem1  45906  supminfrnmpt  45980  supminfxr2  46004  fsumnncl  46109  limcperiod  46165  sumnnodd  46167  limcresiooub  46177  limcresioolb  46178  0ellimcdiv  46184  reclimc  46188  limsupval3  46227  limsupequzmpt2  46253  liminfval5  46300  limsupresxr  46301  liminfresxr  46302  liminfvalxr  46318  liminfequzmpt2  46326  climliminflimsupd  46336  liminfltlem  46339  liminflbuz2  46350  sinmulcos  46400  coskpi2  46401  cncfdmsn  46425  cncfiooicclem1  46428  fprodsubrecnncnvlem  46442  fprodaddrecnncnvlem  46444  fperdvper  46454  dvnmptdivc  46473  dvnxpaek  46477  dvnmul  46478  dvnprodlem1  46481  dvnprodlem3  46483  itgcoscmulx  46504  itgsincmulx  46509  itgspltprt  46514  itgiccshift  46515  itgperiod  46516  sublevolico  46519  volioof  46522  ovolsplit  46523  fvvolioof  46524  fvvolicof  46526  stoweidlem22  46557  stoweidlem32  46567  wallispilem5  46604  stirlinglem5  46613  dirkertrigeqlem2  46634  dirkertrigeq  46636  dirkercncflem1  46638  dirkercncflem2  46639  dirkercncflem4  46641  fourierdlem13  46655  fourierdlem16  46658  fourierdlem19  46661  fourierdlem21  46663  fourierdlem22  46664  fourierdlem28  46670  fourierdlem32  46674  fourierdlem33  46675  fourierdlem42  46684  fourierdlem47  46688  fourierdlem48  46689  fourierdlem49  46690  fourierdlem50  46691  fourierdlem56  46697  fourierdlem60  46701  fourierdlem61  46702  fourierdlem64  46705  fourierdlem66  46707  fourierdlem71  46712  fourierdlem73  46714  fourierdlem74  46715  fourierdlem76  46717  fourierdlem78  46719  fourierdlem79  46720  fourierdlem80  46721  fourierdlem81  46722  fourierdlem83  46724  fourierdlem88  46729  fourierdlem92  46733  fourierdlem93  46734  fourierdlem97  46738  fourierdlem101  46742  fourierdlem103  46744  fourierdlem104  46745  fourierdlem109  46750  fourierdlem111  46752  fouriersw  46766  elaa2lem  46768  etransclem24  46793  etransclem25  46794  etransclem35  46804  etransclem46  46815  rrndistlt  46825  rrxunitopnfi  46827  qndenserrnbl  46830  qndenserrnopnlem  46832  saldifcl2  46863  intsal  46865  sge0sn  46914  sge0ltfirp  46935  sge0iunmptlemre  46950  sge0fodjrnlem  46951  sge0isum  46962  sge0xaddlem1  46968  nnfoctbdjlem  46990  meassle  46998  ismeannd  47002  meadif  47014  meaiuninclem  47015  meaiininclem  47021  omeunile  47040  caragendifcl  47049  caratheodory  47063  isomenndlem  47065  ovnsubaddlem1  47105  hoidmv1lelem2  47127  hoidmv1le  47129  hoidmvlelem2  47131  hoidmvle  47135  hoi2toco  47142  rrnmbl  47149  hoidifhspdmvle  47155  voncmpl  47156  hoiqssbl  47160  hspmbllem1  47161  hspmbllem2  47162  ovolval2lem  47178  ovolval5lem2  47188  ovnovollem1  47191  ovnovollem2  47192  hoimbl2  47200  vonhoire  47207  salpreimagelt  47242  salpreimalegt  47244  preimaioomnf  47254  smfres  47325  smfmullem1  47326  smflimmpt  47345  smfsupmpt  47350  smfinfmpt  47354  smflimsupmpt  47364  smfliminflem  47365  smfliminfmpt  47367  sigarcol  47399  sin5tlem2  47429  f1oresf1o  47845  elsprel  48042  prproropf1o  48074  paireqne  48078  sfprmdvdsmersenne  48173  lighneallem3  48177  lighneallem4  48180  nprmdvdsfacm1lem1  48190  nn0onn0exALTV  48282  nnsum3primesprm  48373  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  isuspgrim0lem  48476  clnbgrgrimlem  48516  uspgrlimlem3  48573  uspgrlimlem4  48574  gpgedgvtx0  48644  gpgedgvtx1  48645  funcringcsetcALTV2lem7  48879  funcringcsetclem7ALTV  48902  lincext3  49039  lincresunit3  49064  nn0onn0ex  49106  nnpw2pmod  49166  blennn0em1  49174  digexp  49190  dignn0ehalf  49200  nn0mulfsum  49207  itcovalpclem1  49253  eenglngeehlnmlem2  49321  rrx2vlinest  49324  line2  49335  itschlc0xyqsol  49350  itsclinecirc0b  49357  toplatjoin  49584  toplatmeet  49585  upeu2lem  49610  oppff1o  49731  imaf1co  49737  upciclem3  49750  natoppfb  49813  oppcthinco  50021  oppcthinendcALT  50023  lmddu  50249  recsec  50338  reccsc  50339  aacllem  50383  amgmlemALT  50385