Theorem eqtr2d 2773

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtrrd  2777  3eqtr2rd  2779  ifan  4535  ifor  4536  dfopif  4828  fnco  6618  fnsnfv  6921  nvocnv  7237  elovmpt3rab1  7628  onsucmin  7773  csbopeq1a  8004  oaabs2  8587  ecinxp  8741  resixpfo  8886  sbthlem3  9029  rankxpsuc  9806  fseqenlem2  9947  dfac2b  10053  isf32lem9  10283  compsscnvlem  10292  ttukeylem7  10437  fpwwe2lem10  10563  00id  11320  submul2  11589  mulsubfacd  11610  divadddiv  11868  infrenegsup  12137  xadd4d  13230  fzdifsuc  13512  fzval3  13662  fzoshftral  13715  ceim1l  13779  fldiv  13792  flmod  13817  intfrac  13818  modcyc2  13839  modaddb  13841  moddi  13874  uzrdgfni  13893  axdc4uzlem  13918  seqf1olem1  13976  seqf1olem2  13977  seqid2  13983  expnegz  14031  binom2sub  14155  binom3  14159  hashreshashfun  14374  ccatw2s1p2  14573  ccats1pfxeq  14649  pfxccatin12lem2  14666  pfxccatin12  14668  swrdccat3b  14675  cshweqrep  14756  2cshwcshw  14760  ccatco  14770  swrds2  14875  relexpsucnnr  14960  relexpaddnn  14986  reim  15044  mulre  15056  addcj  15083  absimle  15244  clim2ser  15590  isercoll2  15604  serf0  15616  iseralt  15620  summolem3  15649  isumclim3  15694  mptfzshft  15713  fsumrev  15714  fsum2mul  15724  incexc  15772  isumsplit  15775  mertenslem1  15819  fprodrev  15912  iprodclim3  15935  binomfallfaclem2  15975  ef4p  16050  tanval3  16071  efival  16089  sinmul  16109  bitsinvp1  16388  sadaddlem  16405  bitsshft  16414  smu01lem  16424  dfgcd2  16485  lcmgcdlem  16545  lcm1  16549  lcmfass  16585  eulerthlem2  16721  hashgcdeq  16729  powm2modprm  16743  pythagtriplem16  16770  pczpre  16787  pcqdiv  16797  pcadd  16829  pcfac  16839  prmreclem5  16860  4sqlem10  16887  4sqlem19  16903  vdwapun  16914  vdwlem1  16921  ramcl  16969  setsstruct  17115  strfvd  17139  strfv2d  17140  xpsff1o  17500  xpsrnbas  17504  2oppccomf  17660  oppcepi  17675  sscfn1  17753  sscfn2  17754  invfuc  17913  funcestrcsetclem7  18081  funcsetcestrclem7  18096  gsumsplit1r  18624  grpinvssd  18959  grpinvval2  18965  cycsubggend  19146  pmtrdifwrdellem2  19423  psgnunilem1  19434  psgnuni  19440  pgp0  19537  sylow1lem1  19539  sylow3lem2  19569  efgredleme  19684  efgcpbllemb  19696  frgpuptinv  19712  frgpup3lem  19718  gexexlem  19793  cyggenod  19825  gsumval3eu  19845  gsumval3  19848  gsumzaddlem  19862  dprd2db  19986  ablsimpgfindlem1  20050  ringinvdv  20362  c0snmgmhm  20410  rngcifuestrc  20584  funcrngcsetc  20585  funcrngcsetcALT  20586  funcringcsetc  20619  lss1d  20926  pwssplit1  21023  rhmqusnsg  21252  rngqiprnglin  21269  znzrh2  21512  regsumsupp  21589  ipassr2  21614  dsmmfi  21705  frlmlss  21718  frlmip  21745  frlmlbs  21764  frlmup3  21767  islindf4  21805  mplcoe3  22005  subrgascl  22033  evlseu  22050  psdadd  22118  ply1sclid  22242  ply1chr  22262  evls1addd  22327  evls1muld  22328  evls1vsca  22329  evls1maprhm  22332  evls1maplmhm  22333  evls1maprnss  22334  evl1maprhm  22335  1marepvmarrepid  22531  madurid  22600  smadiadetlem3  22624  mat2pmatghm  22686  pmatcollpwscmatlem1  22745  pm2mpmhmlem2  22775  cpmadurid  22823  cpmidgsumm2pm  22825  cpmadugsumlemB  22830  cayhamlem2  22840  ntrval2  23007  ordtuni  23146  cnclima  23224  cmpsub  23356  ptbasfi  23537  txbasval  23562  pt1hmeo  23762  alexsubALTlem1  24003  trust  24185  ussid  24216  ressuss  24218  ressprdsds  24327  imasdsf1olem  24329  setsms  24436  tmsxms  24442  tmsxpsmopn  24493  subgnm  24589  tngnm  24607  tngngp2  24608  xrsxmet  24766  xrge0gsumle  24790  metdstri  24808  xrhmeo  24912  lebnumlem3  24930  pcorevlem  24994  pi1xfrcnvlem  25024  clmabs  25051  cvsmuleqdivd  25102  rrxip  25358  rrxds  25361  rrxdsfi  25379  minveclem4a  25398  pjthlem1  25405  divcncf  25416  ovolunlem1a  25465  mbfres2  25614  i1faddlem  25662  ibladdlem  25789  iblabs  25798  ditgsplit  25830  dvmptresicc  25885  dvnres  25901  dvmptdiv  25946  dveflem  25951  dveq0  25973  dvfsumabs  25997  itgsubstlem  26023  ply1divex  26110  r1pid2  26135  dgrco  26249  plycjlem  26250  taylthlem1  26349  pserdv2  26408  abelthlem6  26414  abelthlem7  26416  tangtx  26482  abssinper  26498  sineq0  26501  explog  26571  reexplog  26572  eflogeq  26579  abslogle  26595  tanarg  26596  logtayl  26637  logtayl2  26639  relogbdiv  26757  ang180lem3  26789  affineequiv  26801  affineequiv2  26802  chordthmlem4  26813  chordthmlem5  26814  heron  26816  dcubic1lem  26821  dcubic2  26822  dcubic  26824  mcubic  26825  cubic2  26826  dquartlem1  26829  dquart  26831  quart1lem  26833  quartlem1  26835  quart  26839  acoscos  26871  atanlogaddlem  26891  atantayl2  26916  atantayl3  26917  birthdaylem2  26930  efrlim  26947  efrlimOLD  26948  amgmlem  26968  logdifbnd  26972  emcllem3  26976  emcllem6  26979  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  gamigam  27031  lgamcvg2  27033  gamfac  27045  basellem3  27061  basellem8  27066  basellem9  27067  chtprm  27131  logfaclbnd  27201  perfect1  27207  bcp1ctr  27258  bclbnd  27259  bposlem1  27263  lgsdilem  27303  lgsdirnn0  27323  lgsdinn0  27324  gausslemma2dlem1a  27344  gausslemma2dlem4  27348  gausslemma2dlem5a  27349  lgseisenlem2  27355  lgsquadlem1  27359  2sqlem2  27397  mul2sq  27398  2sqmod  27415  2sqnn0  27417  vmadivsum  27461  rpvmasumlem  27466  dchrisumlem1  27468  dchrisumlem2  27469  dchrmusum2  27473  dchrvmasum2if  27476  dchrisum0lem2  27497  logsqvma2  27522  selberg3  27538  selberg4lem1  27539  pntrsumo1  27544  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntibndlem2  27570  pntlemk  27585  pntlemo  27586  ostth2lem4  27615  ostth3  27617  subsfo  28073  negsval2  28074  ltonold  28269  noseqrdgfn  28314  n0fincut  28363  addhalfcut  28467  bdayfinbndlem1  28475  z12shalf  28488  tgbtwndiff  28590  tgifscgr  28592  trgcgrg  28599  motcgr3  28629  tgbtwnconn1lem1  28656  tgbtwnconn1lem2  28657  ismir  28743  miriso  28754  midexlem  28776  ragmir  28784  footexALT  28802  footexlem1  28803  footexlem2  28804  colperpexlem3  28816  mideulem2  28818  midex  28821  opphllem3  28833  midcgr  28864  lmiisolem  28880  brbtwn2  28990  colinearalglem4  28994  axsegconlem1  29002  axpaschlem  29025  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  ushgredgedgloop  29316  crctcshwlkn0lem6  29900  wwlknlsw  29932  wwlksnextwrd  29982  clwlkclwwlklem2a3  30081  clwlkclwwlk2  30090  clwwlkel  30133  clwwlkfo  30137  clwwlkext2edg  30143  eupth2eucrct  30304  numclwwlk2lem1lem  30429  numclwwlk1lem2fo  30445  numclwlk2lem2f  30464  grpoidinvlem2  30593  nvmtri  30759  cnnvm  30770  nvnd  30776  ipidsq  30798  ipnm  30799  ipipcj  30803  blocnilem  30892  ipasslem2  30920  dipsubdir  30936  hvaddsubval  31121  pjhthlem1  31479  pjspansn  31665  pjo  31759  unoplin  32008  adjadj  32024  hmoplin  32030  eigvec1  32050  lnopeqi  32096  nmcexi  32114  lnfnsubi  32134  riesz3i  32150  kbass6  32209  leoprf2  32215  leoprf  32216  pjnmopi  32236  mdslmd1lem1  32413  mdslmd1lem2  32414  superpos  32442  ifeq3da  32633  fresunsn  32715  fgreu  32761  cocnvf1o  32819  resf1o  32820  quad3d  32840  fprodex01  32917  sgnmul  32927  ccatws1f1o  33044  wrdt2ind  33046  mndlactfo  33120  mndractfo  33122  gsummpt2d  33143  gsummptp1  33151  xrge0tsmseq  33169  gsumwrd2dccatlem  33171  gsumwrd2dccat  33172  symgfcoeu  33176  wrdpmtrlast  33187  psgnfzto1stlem  33194  psgnfzto1st  33199  cycpm2tr  33213  cycpmco2lem6  33225  cycpmco2lem7  33226  subrgchr  33331  elrgspnlem1  33336  elrgspnlem3  33338  elrgspnsubrunlem1  33341  rloccring  33364  rhmdvd  33417  qusrn  33502  nsgqusf1olem3  33508  rhmquskerlem  33518  elrspunsn  33522  mxidlirredi  33564  qsdrngi  33588  1arithidomlem1  33628  1arithidomlem2  33629  evls1subd  33665  deg1prod  33676  r1pid2OLD  33702  evlextv  33719  psrmonprod  33729  esplyfval1  33750  esplyind  33752  esplyindfv  33753  esplyfvn  33754  vietalem  33756  resssra  33764  dimval  33778  dimvalfi  33779  lindsunlem  33802  dimkerim  33805  qusdimsum  33806  fedgmullem1  33807  extdg1id  33844  fldextrspunlsplem  33851  fldextrspunlsp  33852  fldextrspunlem1  33853  fldextrspundgdvds  33859  extdgfialglem1  33870  extdgfialglem2  33871  ply1annidllem  33879  algextdeglem4  33898  constrrtcc  33913  constrsslem  33919  constrresqrtcl  33955  cos9thpiminplylem2  33961  cos9thpiminply  33966  madjusmdetlem2  34006  qtophaus  34014  zarclssn  34051  zarcmplem  34059  pstmval  34073  mndpluscn  34104  qqhucn  34170  esumval  34224  gsumesum  34237  esumcst  34241  esumpcvgval  34256  oddpwdc  34532  eulerpartlemgvv  34554  probdif  34598  signsvtn  34762  actfunsnf1o  34782  reprpmtf1o  34804  hgt750lemd  34826  logdivsqrle  34828  hgt750lemg  34832  hgt750lemb  34834  bnj1415  35214  swrdrevpfx  35333  pfxwlk  35340  derangen2  35390  subfaclefac  35392  subfaclim  35404  satom  35572  fmla  35597  mrsubrn  35729  sinccvglem  35888  bcprod  35954  filnetlem4  36597  curunc  37853  ltflcei  37859  matunitlindflem1  37867  matunitlindflem2  37868  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem24  37895  mblfinlem4  37911  ibladdnclem  37927  iblabsnc  37935  iblmulc2nc  37936  ftc1anclem6  37949  ftc1anclem8  37951  sdclem2  37993  ismtycnv  38053  heiborlem10  38071  lflvsass  39457  lkrscss  39474  eqlkr  39475  eqlkr3  39477  ldualvsdi2  39520  omllaw3  39621  cmtcomlemN  39624  cmtbr3N  39630  omlfh3N  39635  llnexchb2lem  40244  dalawlem7  40253  dalawlem11  40257  dalawlem12  40258  pol1N  40286  paddatclN  40325  4atexlemcnd  40448  ltrncoidN  40504  cdleme3b  40605  cdleme11  40646  cdleme15a  40650  cdleme22e  40720  cdleme22g  40724  cdlemg18b  41055  trlcoat  41099  cdlemk2  41208  cdlemk4  41210  cdlemki  41217  cdlemksv2  41223  cdlemk15  41231  cdlemk55a  41335  diainN  41433  dia2dimlem3  41442  dia2dimlem5  41444  dvhlveclem  41484  diaocN  41501  cdlemn4  41574  cdlemn8  41580  dihopelvalcpre  41624  dihmeetlem9N  41691  dih1dimatlem  41705  dihpN  41712  dochvalr3  41739  dochsat  41759  djhjlj  41779  dochdmm1  41786  dihjatcclem4  41797  dihjat1  41805  dihjat4  41809  dochsnkr2cl  41850  dochfl1  41852  lclkrlem2j  41892  mapdordlem2  42013  mapdrvallem2  42021  hdmap10  42216  lcmineqlem12  42410  3lexlogpow5ineq5  42430  aks4d1p1  42446  primrootsunit1  42467  primrootscoprmpow  42469  posbezout  42470  aks6d1c1p3  42480  aks6d1c1p4  42481  aks6d1c1p5  42482  aks6d1c1p7  42483  evl1gprodd  42487  hashscontpow1  42491  aks6d1c3  42493  aks6d1c2lem3  42496  aks6d1c2lem4  42497  aks6d1c2  42500  aks6d1c5lem3  42507  aks6d1c6lem1  42540  aks6d1c6isolem3  42546  aks6d1c6lem5  42547  bcle2d  42549  aks6d1c7lem1  42550  aks5lem3a  42559  grpods  42564  unitscyglem1  42565  unitscyglem2  42566  unitscyglem4  42568  unitscyglem5  42569  aks5lem7  42570  nicomachus  42682  sumcubes  42683  cnreeu  42860  frlmvscadiccat  42876  grpcominv1  42878  riccrng1  42891  ricdrng1  42898  frlmsnic  42910  evlselv  42945  fsuppind  42948  flt4lem7  43017  negexpidd  43039  3cubeslem2  43042  3cubeslem3r  43044  mzpsubmpt  43100  irrapxlem3  43181  pellexlem6  43191  pell1234qrne0  43210  pell1234qrreccl  43211  pell1234qrmulcl  43212  pell14qrdich  43226  pell1qrgaplem  43230  rmxluc  43293  rmyluc  43294  jm2.24nn  43316  jm2.18  43345  jm2.19lem2  43347  jm2.19lem3  43348  jm2.22  43352  jm2.23  43353  jm2.16nn0  43361  jm2.27c  43364  fnwe2lem2  43408  lmhmfgsplit  43443  hbtlem2  43481  onsucf1lem  43626  ofoafo  43713  naddcnffo  43721  naddwordnexlem4  43758  reabssgn  43992  relexpmulnn  44065  relexpmulg  44066  ntrclsneine0lem  44420  int-addassocd  44530  dvconstbi  44690  bccm1k  44698  binomcxplemnotnn0  44712  fmptsnxp  45528  wessf1ornlem  45544  projf1o  45555  infnsuprnmpt  45608  lefldiveq  45654  lt4addmuld  45668  fzdifsuc2  45672  suplesup  45698  infrpge  45710  xrlexaddrp  45711  xralrple2  45713  infleinflem1  45728  supminfrnmpt  45803  supminfxr2  45827  fsumnncl  45932  limcperiod  45988  sumnnodd  45990  limcresiooub  46000  limcresioolb  46001  0ellimcdiv  46007  reclimc  46011  limsupval3  46050  limsupequzmpt2  46076  liminfval5  46123  limsupresxr  46124  liminfresxr  46125  liminfvalxr  46141  liminfequzmpt2  46149  climliminflimsupd  46159  liminfltlem  46162  liminflbuz2  46173  sinmulcos  46223  coskpi2  46224  cncfdmsn  46248  cncfiooicclem1  46251  fprodsubrecnncnvlem  46265  fprodaddrecnncnvlem  46267  fperdvper  46277  dvnmptdivc  46296  dvnxpaek  46300  dvnmul  46301  dvnprodlem1  46304  dvnprodlem3  46306  itgcoscmulx  46327  itgsincmulx  46332  itgspltprt  46337  itgiccshift  46338  itgperiod  46339  sublevolico  46342  volioof  46345  ovolsplit  46346  fvvolioof  46347  fvvolicof  46349  stoweidlem22  46380  stoweidlem32  46390  wallispilem5  46427  stirlinglem5  46436  dirkertrigeqlem2  46457  dirkertrigeq  46459  dirkercncflem1  46461  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem13  46478  fourierdlem16  46481  fourierdlem19  46484  fourierdlem21  46486  fourierdlem22  46487  fourierdlem28  46493  fourierdlem32  46497  fourierdlem33  46498  fourierdlem42  46507  fourierdlem47  46511  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem56  46520  fourierdlem60  46524  fourierdlem61  46525  fourierdlem64  46528  fourierdlem66  46530  fourierdlem71  46535  fourierdlem73  46537  fourierdlem74  46538  fourierdlem76  46540  fourierdlem78  46542  fourierdlem79  46543  fourierdlem80  46544  fourierdlem81  46545  fourierdlem83  46547  fourierdlem88  46552  fourierdlem92  46556  fourierdlem93  46557  fourierdlem97  46561  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  fourierdlem109  46573  fourierdlem111  46575  fouriersw  46589  elaa2lem  46591  etransclem24  46616  etransclem25  46617  etransclem35  46627  etransclem46  46638  rrndistlt  46648  rrxunitopnfi  46650  qndenserrnbl  46653  qndenserrnopnlem  46655  saldifcl2  46686  intsal  46688  sge0sn  46737  sge0ltfirp  46758  sge0iunmptlemre  46773  sge0fodjrnlem  46774  sge0isum  46785  sge0xaddlem1  46791  nnfoctbdjlem  46813  meassle  46821  ismeannd  46825  meadif  46837  meaiuninclem  46838  meaiininclem  46844  omeunile  46863  caragendifcl  46872  caratheodory  46886  isomenndlem  46888  ovnsubaddlem1  46928  hoidmv1lelem2  46950  hoidmv1le  46952  hoidmvlelem2  46954  hoidmvle  46958  hoi2toco  46965  rrnmbl  46972  hoidifhspdmvle  46978  voncmpl  46979  hoiqssbl  46983  hspmbllem1  46984  hspmbllem2  46985  ovolval2lem  47001  ovolval5lem2  47011  ovnovollem1  47014  ovnovollem2  47015  hoimbl2  47023  vonhoire  47030  salpreimagelt  47065  salpreimalegt  47067  preimaioomnf  47077  smfres  47148  smfmullem1  47149  smflimmpt  47168  smfsupmpt  47173  smfinfmpt  47177  smflimsupmpt  47187  smfliminflem  47188  smfliminfmpt  47190  sigarcol  47222  f1oresf1o  47650  elsprel  47835  prproropf1o  47867  paireqne  47871  sfprmdvdsmersenne  47963  lighneallem3  47967  lighneallem4  47970  nn0onn0exALTV  48059  nnsum3primesprm  48150  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  isuspgrim0lem  48253  clnbgrgrimlem  48293  uspgrlimlem3  48350  uspgrlimlem4  48351  gpgedgvtx0  48421  gpgedgvtx1  48422  funcringcsetcALTV2lem7  48656  funcringcsetclem7ALTV  48679  lincext3  48816  lincresunit3  48841  nn0onn0ex  48883  nnpw2pmod  48943  blennn0em1  48951  digexp  48967  dignn0ehalf  48977  nn0mulfsum  48984  itcovalpclem1  49030  eenglngeehlnmlem2  49098  rrx2vlinest  49101  line2  49112  itschlc0xyqsol  49127  itsclinecirc0b  49134  toplatjoin  49361  toplatmeet  49362  upeu2lem  49387  oppff1o  49508  imaf1co  49514  upciclem3  49527  natoppfb  49590  oppcthinco  49798  oppcthinendcALT  49800  lmddu  50026  recsec  50115  reccsc  50116  aacllem  50160  amgmlemALT  50162