Theorem eqtr2d 2777

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 2776	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2742	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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728

This theorem is referenced by:  3eqtrrd  2781  3eqtr2rd  2783  ifan  4526  ifor  4527  dfopif  4814  fnco  6601  fnsnfv  6903  nvocnv  7209  elovmpt3rab1  7591  onsucmin  7734  csbopeq1a  7959  oaabs2  8550  ecinxp  8652  fsetfocdm  8720  resixpfo  8795  sbthlem3  8950  rankxpsuc  9739  fseqenlem2  9882  dfac2b  9987  isf32lem9  10218  compsscnvlem  10227  ttukeylem7  10372  fpwwe2lem10  10497  00id  11251  submul2  11516  mulsubfacd  11537  divadddiv  11791  infrenegsup  12059  xadd4d  13138  fzdifsuc  13417  fzval3  13557  fzoshftral  13605  ceim1l  13668  fldiv  13681  flmod  13706  intfrac  13707  modcyc2  13728  moddi  13760  uzrdgfni  13779  axdc4uzlem  13804  seqf1olem1  13863  seqf1olem2  13864  seqid2  13870  expnegz  13918  binom2sub  14036  binom3  14040  hashreshashfun  14254  ccatw2s1p2  14446  ccats1pfxeq  14525  pfxccatin12lem2  14542  pfxccatin12  14544  swrdccat3b  14551  cshweqrep  14632  2cshwcshw  14637  ccatco  14647  swrds2  14752  relexpsucnnr  14835  relexpaddnn  14861  reim  14919  mulre  14931  addcj  14958  absimle  15120  clim2ser  15465  isercoll2  15479  serf0  15491  iseralt  15495  summolem3  15525  isumclim3  15570  mptfzshft  15589  fsumrev  15590  fsum2mul  15600  incexc  15648  isumsplit  15651  mertenslem1  15695  fprodrev  15786  iprodclim3  15809  binomfallfaclem2  15849  ef4p  15921  tanval3  15942  efival  15960  sinmul  15980  bitsinvp1  16255  sadaddlem  16272  bitsshft  16281  smu01lem  16291  dfgcd2  16353  lcmgcdlem  16408  lcm1  16412  lcmfass  16448  eulerthlem2  16580  hashgcdeq  16587  powm2modprm  16601  pythagtriplem16  16628  pczpre  16645  pcqdiv  16655  pcadd  16687  pcfac  16697  prmreclem5  16718  4sqlem10  16745  4sqlem19  16761  vdwapun  16772  vdwlem1  16779  ramcl  16827  setsstruct  16974  strfvd  16999  strfv2d  17000  xpsff1o  17375  xpsrnbas  17379  2oppccomf  17533  oppcepi  17548  sscfn1  17626  sscfn2  17627  invfuc  17789  funcestrcsetclem7  17960  funcsetcestrclem7  17975  gsumsplit1r  18468  grpinvssd  18748  grpinvval2  18754  cycsubggend  18920  pmtrdifwrdellem2  19186  psgnunilem1  19197  psgnuni  19203  pgp0  19297  sylow1lem1  19299  sylow3lem2  19329  efgredleme  19444  efgcpbllemb  19456  frgpuptinv  19472  frgpup3lem  19478  gexexlem  19548  cyggenod  19579  gsumval3eu  19600  gsumval3  19603  gsumzaddlem  19617  dprd2db  19741  ablsimpgfindlem1  19805  ringinvdv  20031  lss1d  20331  pwssplit1  20427  znzrh2  20859  regsumsupp  20933  ipassr2  20958  dsmmfi  21051  frlmlss  21064  frlmip  21091  frlmlbs  21110  frlmup3  21113  islindf4  21151  mplcoe3  21345  subrgascl  21380  evlseu  21399  ply1sclid  21565  1marepvmarrepid  21830  madurid  21899  smadiadetlem3  21923  mat2pmatghm  21985  pmatcollpwscmatlem1  22044  pm2mpmhmlem2  22074  cpmadurid  22122  cpmidgsumm2pm  22124  cpmadugsumlemB  22129  cayhamlem2  22139  ntrval2  22308  ordtuni  22447  cnclima  22525  cmpsub  22657  ptbasfi  22838  txbasval  22863  pt1hmeo  23063  alexsubALTlem1  23304  trust  23487  ussid  23518  ressuss  23520  ressprdsds  23630  imasdsf1olem  23632  setsms  23741  tmsxms  23748  tmsxpsmopn  23799  subgnm  23895  tngnm  23921  tngngp2  23922  xrsxmet  24078  xrge0gsumle  24102  metdstri  24120  xrhmeo  24215  lebnumlem3  24232  pcorevlem  24295  pi1xfrcnvlem  24325  clmabs  24352  cvsmuleqdivd  24403  rrxip  24660  rrxds  24663  rrxdsfi  24681  minveclem4a  24700  pjthlem1  24707  divcncf  24717  ovolunlem1a  24766  mbfres2  24915  i1faddlem  24963  ibladdlem  25090  iblabs  25099  ditgsplit  25131  dvmptresicc  25186  dvnres  25201  dvmptdiv  25244  dveflem  25249  dveq0  25270  dvfsumabs  25293  itgsubstlem  25318  ply1divex  25407  dgrco  25542  plycjlem  25543  taylthlem1  25638  pserdv2  25695  abelthlem6  25701  abelthlem7  25703  tangtx  25768  abssinper  25783  sineq0  25786  explog  25855  reexplog  25856  eflogeq  25863  abslogle  25879  tanarg  25880  logtayl  25921  logtayl2  25923  relogbdiv  26035  ang180lem3  26067  affineequiv  26079  affineequiv2  26080  chordthmlem4  26091  chordthmlem5  26092  heron  26094  dcubic1lem  26099  dcubic2  26100  dcubic  26102  mcubic  26103  cubic2  26104  dquartlem1  26107  dquart  26109  quart1lem  26111  quartlem1  26113  quart  26117  acoscos  26149  atanlogaddlem  26169  atantayl2  26194  atantayl3  26195  birthdaylem2  26208  efrlim  26225  amgmlem  26245  logdifbnd  26249  emcllem3  26253  emcllem6  26256  lgamgulmlem2  26285  lgamgulmlem3  26286  lgamgulmlem4  26287  lgamgulmlem5  26288  gamigam  26308  lgamcvg2  26310  gamfac  26322  basellem3  26338  basellem8  26343  basellem9  26344  chtprm  26408  logfaclbnd  26476  perfect1  26482  bcp1ctr  26533  bclbnd  26534  bposlem1  26538  lgsdilem  26578  lgsdirnn0  26598  lgsdinn0  26599  gausslemma2dlem1a  26619  gausslemma2dlem4  26623  gausslemma2dlem5a  26624  lgseisenlem2  26630  lgsquadlem1  26634  2sqlem2  26672  mul2sq  26673  2sqmod  26690  2sqnn0  26692  vmadivsum  26736  rpvmasumlem  26741  dchrisumlem1  26743  dchrisumlem2  26744  dchrmusum2  26748  dchrvmasum2if  26751  dchrisum0lem2  26772  logsqvma2  26797  selberg3  26813  selberg4lem1  26814  pntrsumo1  26819  pntrlog2bndlem2  26832  pntrlog2bndlem3  26833  pntrlog2bndlem5  26835  pntibndlem2  26845  pntlemk  26860  pntlemo  26861  ostth2lem4  26890  ostth3  26892  tgbtwndiff  27156  tgifscgr  27158  trgcgrg  27165  motcgr3  27195  tgbtwnconn1lem1  27222  tgbtwnconn1lem2  27223  ismir  27309  miriso  27320  midexlem  27342  ragmir  27350  footexALT  27368  footexlem1  27369  footexlem2  27370  colperpexlem3  27382  mideulem2  27384  midex  27387  opphllem3  27399  midcgr  27430  lmiisolem  27446  brbtwn2  27562  colinearalglem4  27566  axsegconlem1  27574  axpaschlem  27597  axcontlem4  27624  axcontlem7  27627  axcontlem8  27628  ushgredgedgloop  27887  crctcshwlkn0lem6  28468  wwlknlsw  28500  wwlksnextwrd  28550  clwlkclwwlklem2a3  28646  clwlkclwwlk2  28655  clwwlkel  28698  clwwlkfo  28702  clwwlkext2edg  28708  eupth2eucrct  28869  numclwwlk2lem1lem  28994  numclwwlk1lem2fo  29010  numclwlk2lem2f  29029  grpoidinvlem2  29155  nvmtri  29321  cnnvm  29332  nvnd  29338  ipidsq  29360  ipnm  29361  ipipcj  29365  blocnilem  29454  ipasslem2  29482  dipsubdir  29498  hvaddsubval  29683  pjhthlem1  30041  pjspansn  30227  pjo  30321  unoplin  30570  adjadj  30586  hmoplin  30592  eigvec1  30612  lnopeqi  30658  nmcexi  30676  lnfnsubi  30696  riesz3i  30712  kbass6  30771  leoprf2  30777  leoprf  30778  pjnmopi  30798  mdslmd1lem1  30975  mdslmd1lem2  30976  superpos  31004  ifeq3da  31176  fgreu  31296  resf1o  31352  fprodex01  31426  wrdt2ind  31512  gsummpt2d  31596  xrge0tsmseq  31606  symgfcoeu  31638  psgnfzto1stlem  31654  psgnfzto1st  31659  cycpm2tr  31673  cycpmco2lem6  31685  cycpmco2lem7  31686  subrgchr  31778  rhmdvd  31817  nsgqusf1olem3  31897  ply1chr  31966  dimval  31984  dimvalfi  31985  lindsunlem  32003  dimkerim  32006  qusdimsum  32007  fedgmullem1  32008  extdg1id  32036  madjusmdetlem2  32076  qtophaus  32084  zarclssn  32121  zarcmplem  32129  pstmval  32143  mndpluscn  32174  qqhucn  32240  esumval  32312  gsumesum  32325  esumcst  32329  esumpcvgval  32344  oddpwdc  32621  eulerpartlemgvv  32643  probdif  32687  sgnmul  32809  signsvtn  32863  actfunsnf1o  32884  reprpmtf1o  32906  hgt750lemd  32928  logdivsqrle  32930  hgt750lemg  32934  hgt750lemb  32936  bnj1415  33317  swrdrevpfx  33377  pfxwlk  33384  derangen2  33435  subfaclefac  33437  subfaclim  33449  satom  33617  fmla  33642  mrsubrn  33774  sinccvglem  33929  bcprod  33994  filnetlem4  34666  curunc  35864  ltflcei  35870  matunitlindflem1  35878  matunitlindflem2  35879  poimirlem16  35898  poimirlem17  35899  poimirlem19  35901  poimirlem20  35902  poimirlem24  35906  mblfinlem4  35922  ibladdnclem  35938  iblabsnc  35946  iblmulc2nc  35947  ftc1anclem6  35960  ftc1anclem8  35962  sdclem2  36005  ismtycnv  36065  heiborlem10  36083  lflvsass  37348  lkrscss  37365  eqlkr  37366  eqlkr3  37368  ldualvsdi2  37411  omllaw3  37512  cmtcomlemN  37515  cmtbr3N  37521  omlfh3N  37526  llnexchb2lem  38136  dalawlem7  38145  dalawlem11  38149  dalawlem12  38150  pol1N  38178  paddatclN  38217  4atexlemcnd  38340  ltrncoidN  38396  cdleme3b  38497  cdleme11  38538  cdleme15a  38542  cdleme22e  38612  cdleme22g  38616  cdlemg18b  38947  trlcoat  38991  cdlemk2  39100  cdlemk4  39102  cdlemki  39109  cdlemksv2  39115  cdlemk15  39123  cdlemk55a  39227  diainN  39325  dia2dimlem3  39334  dia2dimlem5  39336  dvhlveclem  39376  diaocN  39393  cdlemn4  39466  cdlemn8  39472  dihopelvalcpre  39516  dihmeetlem9N  39583  dih1dimatlem  39597  dihpN  39604  dochvalr3  39631  dochsat  39651  djhjlj  39671  dochdmm1  39678  dihjatcclem4  39689  dihjat1  39697  dihjat4  39701  dochsnkr2cl  39742  dochfl1  39744  lclkrlem2j  39784  mapdordlem2  39905  mapdrvallem2  39913  hdmap10  40108  lcmineqlem12  40302  3lexlogpow5ineq5  40322  aks4d1p1  40338  frlmvscadiccat  40491  riccrng1  40506  frlmsnic  40523  fsuppind  40539  mhphf  40545  cnreeu  40698  flt4lem7  40758  negexpidd  40766  3cubeslem2  40769  3cubeslem3r  40771  mzpsubmpt  40827  irrapxlem3  40908  pellexlem6  40918  pell1234qrne0  40937  pell1234qrreccl  40938  pell1234qrmulcl  40939  pell14qrdich  40953  pell1qrgaplem  40957  rmxluc  41021  rmyluc  41022  jm2.24nn  41044  jm2.18  41073  jm2.19lem2  41075  jm2.19lem3  41076  jm2.22  41080  jm2.23  41081  jm2.16nn0  41089  jm2.27c  41092  fnwe2lem2  41139  lmhmfgsplit  41174  hbtlem2  41212  ofoafo  41322  naddcnffo  41330  reabssgn  41565  relexpmulnn  41638  relexpmulg  41639  ntrclsneine0lem  41995  int-addassocd  42106  dvconstbi  42273  bccm1k  42281  binomcxplemnotnn0  42295  fmptsnxp  43032  wessf1ornlem  43049  projf1o  43063  infnsuprnmpt  43124  lefldiveq  43166  lt4addmuld  43180  fzdifsuc2  43184  suplesup  43213  infrpge  43225  xrlexaddrp  43226  xralrple2  43228  infleinflem1  43244  supminfrnmpt  43320  supminfxr2  43344  fsumnncl  43449  limcperiod  43505  sumnnodd  43507  limcresiooub  43519  limcresioolb  43520  0ellimcdiv  43526  reclimc  43530  limsupval3  43569  limsupequzmpt2  43595  liminfval5  43642  limsupresxr  43643  liminfresxr  43644  liminfvalxr  43660  liminfequzmpt2  43668  climliminflimsupd  43678  liminfltlem  43681  liminflbuz2  43692  sinmulcos  43742  coskpi2  43743  cncfdmsn  43767  cncfiooicclem1  43770  fprodsubrecnncnvlem  43784  fprodaddrecnncnvlem  43786  fperdvper  43796  dvnmptdivc  43815  dvnxpaek  43819  dvnmul  43820  dvnprodlem1  43823  dvnprodlem3  43825  itgcoscmulx  43846  itgsincmulx  43851  itgspltprt  43856  itgiccshift  43857  itgperiod  43858  sublevolico  43861  volioof  43864  ovolsplit  43865  fvvolioof  43866  fvvolicof  43868  stoweidlem22  43899  stoweidlem32  43909  wallispilem5  43946  stirlinglem5  43955  dirkertrigeqlem2  43976  dirkertrigeq  43978  dirkercncflem1  43980  dirkercncflem2  43981  dirkercncflem4  43983  fourierdlem13  43997  fourierdlem16  44000  fourierdlem19  44003  fourierdlem21  44005  fourierdlem22  44006  fourierdlem28  44012  fourierdlem32  44016  fourierdlem33  44017  fourierdlem42  44026  fourierdlem47  44030  fourierdlem48  44031  fourierdlem49  44032  fourierdlem50  44033  fourierdlem56  44039  fourierdlem60  44043  fourierdlem61  44044  fourierdlem64  44047  fourierdlem66  44049  fourierdlem71  44054  fourierdlem73  44056  fourierdlem74  44057  fourierdlem76  44059  fourierdlem78  44061  fourierdlem79  44062  fourierdlem80  44063  fourierdlem81  44064  fourierdlem83  44066  fourierdlem88  44071  fourierdlem92  44075  fourierdlem93  44076  fourierdlem97  44080  fourierdlem101  44084  fourierdlem103  44086  fourierdlem104  44087  fourierdlem109  44092  fourierdlem111  44094  fouriersw  44108  elaa2lem  44110  etransclem24  44135  etransclem25  44136  etransclem35  44146  etransclem46  44157  rrndistlt  44167  rrxunitopnfi  44169  qndenserrnbl  44172  qndenserrnopnlem  44174  saldifcl2  44203  intsal  44205  sge0sn  44254  sge0ltfirp  44275  sge0iunmptlemre  44290  sge0fodjrnlem  44291  sge0isum  44302  sge0xaddlem1  44308  nnfoctbdjlem  44330  meassle  44338  ismeannd  44342  meadif  44354  meaiuninclem  44355  meaiininclem  44361  omeunile  44380  caragendifcl  44389  caratheodory  44403  isomenndlem  44405  ovnsubaddlem1  44445  hoidmv1lelem2  44467  hoidmv1le  44469  hoidmvlelem2  44471  hoidmvle  44475  hoi2toco  44482  rrnmbl  44489  hoidifhspdmvle  44495  voncmpl  44496  hoiqssbl  44500  hspmbllem1  44501  hspmbllem2  44502  ovolval2lem  44518  ovolval5lem2  44528  ovnovollem1  44531  ovnovollem2  44532  hoimbl2  44540  vonhoire  44547  salpreimagelt  44582  salpreimalegt  44584  preimaioomnf  44594  smfres  44665  smfmullem1  44666  smflimmpt  44685  smfsupmpt  44690  smfinfmpt  44694  smflimsupmpt  44704  smfliminflem  44705  smfliminfmpt  44707  sigarcol  44731  f1oresf1o  45133  elsprel  45278  prproropf1o  45310  paireqne  45314  sfprmdvdsmersenne  45406  lighneallem3  45410  lighneallem4  45413  nn0onn0exALTV  45502  nnsum3primesprm  45593  nnsum4primesodd  45599  nnsum4primesoddALTV  45600  c0snmgmhm  45823  rngcifuestrc  45906  funcrngcsetc  45907  funcrngcsetcALT  45908  funcringcsetc  45944  funcringcsetcALTV2lem7  45951  funcringcsetclem7ALTV  45974  lincext3  46148  lincresunit3  46173  nn0onn0ex  46220  nnpw2pmod  46280  blennn0em1  46288  digexp  46304  dignn0ehalf  46314  nn0mulfsum  46321  itcovalpclem1  46367  eenglngeehlnmlem2  46435  rrx2vlinest  46438  line2  46449  itschlc0xyqsol  46464  itsclinecirc0b  46471  toplatjoin  46639  toplatmeet  46640  recsec  46809  reccsc  46810  aacllem  46856  amgmlemALT  46858