Theorem eqtr2d 2775

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  3eqtrrd  2779  3eqtr2rd  2781  ifan  4508  ifor  4509  dfopif  4801  fnco  6603  fnsnfv  6906  nvocnv  7225  elovmpt3rab1  7616  onsucmin  7761  csbopeq1a  7992  oaabs2  8575  ecinxp  8729  resixpfo  8874  sbthlem3  9017  rankxpsuc  9797  fseqenlem2  9938  dfac2b  10044  isf32lem9  10274  compsscnvlem  10283  ttukeylem7  10428  fpwwe2lem10  10554  00id  11312  submul2  11581  mulsubfacd  11602  divadddiv  11861  infrenegsup  12130  xadd4d  13246  fzdifsuc  13529  fzval3  13680  fzoshftral  13733  ceim1l  13797  fldiv  13810  flmod  13835  intfrac  13836  modcyc2  13857  modaddb  13859  moddi  13892  uzrdgfni  13911  axdc4uzlem  13936  seqf1olem1  13994  seqf1olem2  13995  seqid2  14001  expnegz  14049  binom2sub  14173  binom3  14177  hashreshashfun  14392  ccatw2s1p2  14591  ccats1pfxeq  14667  pfxccatin12lem2  14684  pfxccatin12  14686  swrdccat3b  14693  cshweqrep  14774  2cshwcshw  14778  ccatco  14788  swrds2  14893  relexpsucnnr  14978  relexpaddnn  15004  reim  15062  mulre  15074  addcj  15101  absimle  15262  clim2ser  15608  isercoll2  15622  serf0  15634  iseralt  15638  summolem3  15667  isumclim3  15712  mptfzshft  15731  fsumrev  15732  fsum2mul  15742  incexc  15793  isumsplit  15796  mertenslem1  15840  fprodrev  15933  iprodclim3  15956  binomfallfaclem2  15996  ef4p  16071  tanval3  16092  efival  16110  sinmul  16130  bitsinvp1  16409  sadaddlem  16426  bitsshft  16435  smu01lem  16445  dfgcd2  16506  lcmgcdlem  16566  lcm1  16570  lcmfass  16606  eulerthlem2  16743  hashgcdeq  16751  powm2modprm  16765  pythagtriplem16  16792  pczpre  16809  pcqdiv  16819  pcadd  16851  pcfac  16861  prmreclem5  16882  4sqlem10  16909  4sqlem19  16925  vdwapun  16936  vdwlem1  16943  ramcl  16991  setsstruct  17137  strfvd  17161  strfv2d  17162  xpsff1o  17522  xpsrnbas  17526  2oppccomf  17682  oppcepi  17697  sscfn1  17775  sscfn2  17776  invfuc  17935  funcestrcsetclem7  18103  funcsetcestrclem7  18118  gsumsplit1r  18646  grpinvssd  18984  grpinvval2  18990  cycsubggend  19171  pmtrdifwrdellem2  19448  psgnunilem1  19459  psgnuni  19465  pgp0  19562  sylow1lem1  19564  sylow3lem2  19594  efgredleme  19709  efgcpbllemb  19721  frgpuptinv  19737  frgpup3lem  19743  gexexlem  19818  cyggenod  19850  gsumval3eu  19870  gsumval3  19873  gsumzaddlem  19887  dprd2db  20011  ablsimpgfindlem1  20075  ringinvdv  20385  c0snmgmhm  20433  rngcifuestrc  20611  funcrngcsetc  20612  funcrngcsetcALT  20613  funcringcsetc  20646  lss1d  20953  pwssplit1  21049  rhmqusnsg  21278  rngqiprnglin  21295  znzrh2  21520  regsumsupp  21597  ipassr2  21622  dsmmfi  21713  frlmlss  21726  frlmip  21753  frlmlbs  21772  frlmup3  21775  islindf4  21813  mplcoe3  22014  subrgascl  22042  evlseu  22059  psdadd  22151  ply1sclid  22274  ply1chr  22292  evls1addd  22357  evls1muld  22358  evls1vsca  22359  evls1maprhm  22362  evls1maplmhm  22363  evls1maprnss  22364  evl1maprhm  22365  1marepvmarrepid  22558  madurid  22627  smadiadetlem3  22651  mat2pmatghm  22713  pmatcollpwscmatlem1  22772  pm2mpmhmlem2  22802  cpmadurid  22850  cpmidgsumm2pm  22852  cpmadugsumlemB  22857  cayhamlem2  22867  ntrval2  23034  ordtuni  23173  cnclima  23251  cmpsub  23383  ptbasfi  23564  txbasval  23589  pt1hmeo  23789  alexsubALTlem1  24030  trust  24212  ussid  24243  ressuss  24245  ressprdsds  24354  imasdsf1olem  24356  setsms  24463  tmsxms  24469  tmsxpsmopn  24520  subgnm  24616  tngnm  24634  tngngp2  24635  xrsxmet  24793  xrge0gsumle  24817  metdstri  24835  xrhmeo  24931  lebnumlem3  24948  pcorevlem  25011  pi1xfrcnvlem  25041  clmabs  25068  cvsmuleqdivd  25119  rrxip  25375  rrxds  25378  rrxdsfi  25396  minveclem4a  25415  pjthlem1  25422  divcncf  25432  ovolunlem1a  25481  mbfres2  25630  i1faddlem  25678  ibladdlem  25805  iblabs  25814  ditgsplit  25846  dvmptresicc  25901  dvnres  25916  dvmptdiv  25959  dveflem  25964  dveq0  25985  dvfsumabs  26008  itgsubstlem  26033  ply1divex  26120  r1pid2  26145  dgrco  26258  plycjlem  26259  taylthlem1  26356  pserdv2  26413  abelthlem6  26419  abelthlem7  26421  tangtx  26487  abssinper  26503  sineq0  26506  explog  26576  reexplog  26577  eflogeq  26584  abslogle  26600  tanarg  26601  logtayl  26642  logtayl2  26644  relogbdiv  26761  ang180lem3  26793  affineequiv  26805  affineequiv2  26806  chordthmlem4  26817  chordthmlem5  26818  heron  26820  dcubic1lem  26825  dcubic2  26826  dcubic  26828  mcubic  26829  cubic2  26830  dquartlem1  26833  dquart  26835  quart1lem  26837  quartlem1  26839  quart  26843  acoscos  26875  atanlogaddlem  26895  atantayl2  26920  atantayl3  26921  birthdaylem2  26934  efrlim  26951  amgmlem  26971  logdifbnd  26975  emcllem3  26979  emcllem6  26982  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  gamigam  27034  lgamcvg2  27036  gamfac  27048  basellem3  27064  basellem8  27069  basellem9  27070  chtprm  27134  logfaclbnd  27203  perfect1  27209  bcp1ctr  27260  bclbnd  27261  bposlem1  27265  lgsdilem  27305  lgsdirnn0  27325  lgsdinn0  27326  gausslemma2dlem1a  27346  gausslemma2dlem4  27350  gausslemma2dlem5a  27351  lgseisenlem2  27357  lgsquadlem1  27361  2sqlem2  27399  mul2sq  27400  2sqmod  27417  2sqnn0  27419  vmadivsum  27463  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasum2if  27478  dchrisum0lem2  27499  logsqvma2  27524  selberg3  27540  selberg4lem1  27541  pntrsumo1  27546  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem5  27562  pntibndlem2  27572  pntlemk  27587  pntlemo  27588  ostth2lem4  27617  ostth3  27619  subsfo  28075  negsval2  28076  ltonold  28271  noseqrdgfn  28316  n0fincut  28365  addhalfcut  28469  bdayfinbndlem1  28477  z12shalf  28490  tgbtwndiff  28592  tgifscgr  28594  trgcgrg  28601  motcgr3  28631  tgbtwnconn1lem1  28658  tgbtwnconn1lem2  28659  ismir  28745  miriso  28756  midexlem  28778  ragmir  28786  footexALT  28804  footexlem1  28805  footexlem2  28806  colperpexlem3  28818  mideulem2  28820  midex  28823  opphllem3  28835  midcgr  28866  lmiisolem  28882  brbtwn2  28992  colinearalglem4  28996  axsegconlem1  29004  axpaschlem  29027  axcontlem4  29054  axcontlem7  29057  axcontlem8  29058  ushgredgedgloop  29318  crctcshwlkn0lem6  29901  wwlknlsw  29933  wwlksnextwrd  29983  clwlkclwwlklem2a3  30082  clwlkclwwlk2  30091  clwwlkel  30134  clwwlkfo  30138  clwwlkext2edg  30144  eupth2eucrct  30305  numclwwlk2lem1lem  30430  numclwwlk1lem2fo  30446  numclwlk2lem2f  30465  grpoidinvlem2  30594  nvmtri  30760  cnnvm  30771  nvnd  30777  ipidsq  30799  ipnm  30800  ipipcj  30804  blocnilem  30893  ipasslem2  30921  dipsubdir  30937  hvaddsubval  31122  pjhthlem1  31480  pjspansn  31666  pjo  31760  unoplin  32009  adjadj  32025  hmoplin  32031  eigvec1  32051  lnopeqi  32097  nmcexi  32115  lnfnsubi  32135  riesz3i  32151  kbass6  32210  leoprf2  32216  leoprf  32217  pjnmopi  32237  mdslmd1lem1  32414  mdslmd1lem2  32415  superpos  32443  ifeq3da  32634  fresunsn  32717  fgreu  32763  cocnvf1o  32821  resf1o  32822  quad3d  32841  fprodex01  32917  sgnmul  32927  ccatws1f1o  33030  wrdt2ind  33032  mndlactfo  33106  mndractfo  33108  gsummpt2d  33130  gsummptp1  33138  xrge0tsmseq  33156  gsumwrd2dccatlem  33158  gsumwrd2dccat  33159  symgfcoeu  33163  wrdpmtrlast  33174  psgnfzto1stlem  33181  psgnfzto1st  33186  cycpm2tr  33200  cycpmco2lem6  33212  cycpmco2lem7  33213  subrgchr  33318  elrgspnlem1  33323  elrgspnlem3  33325  elrgspnsubrunlem1  33328  rloccring  33351  rhmdvd  33407  qusrn  33492  nsgqusf1olem3  33498  rhmquskerlem  33508  elrspunsn  33512  mxidlirredi  33554  qsdrngi  33578  1arithidomlem1  33618  1arithidomlem2  33619  evls1subd  33655  deg1prod  33666  r1pid2OLD  33692  0mplrim  33698  evlextv  33726  psrmonprod  33736  esplyfval1  33757  esplyind  33759  esplyindfv  33760  esplyfvn  33761  vietalem  33763  resssra  33771  dimval  33785  dimvalfi  33786  lindsunlem  33808  dimkerim  33811  qusdimsum  33812  fedgmullem1  33813  extdg1id  33850  fldextrspunlsplem  33857  fldextrspunlsp  33858  fldextrspunlem1  33859  fldextrspundgdvds  33865  extdgfialglem1  33876  extdgfialglem2  33877  ply1annidllem  33885  algextdeglem4  33904  constrrtcc  33919  constrsslem  33925  constrresqrtcl  33961  cos9thpiminplylem2  33967  cos9thpiminply  33972  madjusmdetlem2  34012  qtophaus  34020  zarclssn  34057  zarcmplem  34065  pstmval  34079  mndpluscn  34110  qqhucn  34176  esumval  34230  gsumesum  34243  esumcst  34247  esumpcvgval  34262  oddpwdc  34538  eulerpartlemgvv  34560  probdif  34604  signsvtn  34768  actfunsnf1o  34788  reprpmtf1o  34810  hgt750lemd  34832  logdivsqrle  34834  hgt750lemg  34838  hgt750lemb  34840  bnj1415  35220  swrdrevpfx  35345  pfxwlk  35352  derangen2  35402  subfaclefac  35404  subfaclim  35416  satom  35584  fmla  35609  mrsubrn  35741  sinccvglem  35900  bcprod  35966  filnetlem4  36609  curunc  37969  ltflcei  37975  matunitlindflem1  37983  matunitlindflem2  37984  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem24  38011  mblfinlem4  38027  ibladdnclem  38043  iblabsnc  38051  iblmulc2nc  38052  ftc1anclem6  38065  ftc1anclem8  38067  sdclem2  38109  ismtycnv  38169  heiborlem10  38187  lflvsass  39573  lkrscss  39590  eqlkr  39591  eqlkr3  39593  ldualvsdi2  39636  omllaw3  39737  cmtcomlemN  39740  cmtbr3N  39746  omlfh3N  39751  llnexchb2lem  40360  dalawlem7  40369  dalawlem11  40373  dalawlem12  40374  pol1N  40402  paddatclN  40441  4atexlemcnd  40564  ltrncoidN  40620  cdleme3b  40721  cdleme11  40762  cdleme15a  40766  cdleme22e  40836  cdleme22g  40840  cdlemg18b  41171  trlcoat  41215  cdlemk2  41324  cdlemk4  41326  cdlemki  41333  cdlemksv2  41339  cdlemk15  41347  cdlemk55a  41451  diainN  41549  dia2dimlem3  41558  dia2dimlem5  41560  dvhlveclem  41600  diaocN  41617  cdlemn4  41690  cdlemn8  41696  dihopelvalcpre  41740  dihmeetlem9N  41807  dih1dimatlem  41821  dihpN  41828  dochvalr3  41855  dochsat  41875  djhjlj  41895  dochdmm1  41902  dihjatcclem4  41913  dihjat1  41921  dihjat4  41925  dochsnkr2cl  41966  dochfl1  41968  lclkrlem2j  42008  mapdordlem2  42129  mapdrvallem2  42137  hdmap10  42332  lcmineqlem12  42525  3lexlogpow5ineq5  42545  aks4d1p1  42561  primrootsunit1  42582  primrootscoprmpow  42584  posbezout  42585  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1p7  42598  evl1gprodd  42602  hashscontpow1  42606  aks6d1c3  42608  aks6d1c2lem3  42611  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c5lem3  42622  aks6d1c6lem1  42655  aks6d1c6isolem3  42661  aks6d1c6lem5  42662  bcle2d  42664  aks6d1c7lem1  42665  aks5lem3a  42674  grpods  42679  unitscyglem1  42680  unitscyglem2  42681  unitscyglem4  42683  unitscyglem5  42684  aks5lem7  42685  nicomachus  42789  sumcubes  42790  cnreeu  42980  frlmvscadiccat  42996  grpcominv1  42998  riccrng1  43007  ricdrng1  43014  frlmsnic  43026  evlselv  43039  fsuppind  43040  flt4lem7  43109  negexpidd  43131  3cubeslem2  43134  3cubeslem3r  43136  mzpsubmpt  43192  irrapxlem3  43269  pellexlem6  43279  pell1234qrne0  43298  pell1234qrreccl  43299  pell1234qrmulcl  43300  pell14qrdich  43314  pell1qrgaplem  43318  rmxluc  43381  rmyluc  43382  jm2.24nn  43404  jm2.18  43433  jm2.19lem2  43435  jm2.19lem3  43436  jm2.22  43440  jm2.23  43441  jm2.16nn0  43449  jm2.27c  43452  fnwe2lem2  43496  lmhmfgsplit  43531  hbtlem2  43569  onsucf1lem  43714  ofoafo  43801  naddcnffo  43809  naddwordnexlem4  43846  reabssgn  44080  relexpmulnn  44153  relexpmulg  44154  ntrclsneine0lem  44508  int-addassocd  44618  dvconstbi  44778  bccm1k  44786  binomcxplemnotnn0  44800  fmptsnxp  45616  wessf1ornlem  45632  projf1o  45643  infnsuprnmpt  45694  lefldiveq  45740  lt4addmuld  45754  fzdifsuc2  45758  suplesup  45784  infrpge  45796  xrlexaddrp  45797  xralrple2  45799  infleinflem1  45814  supminfrnmpt  45888  supminfxr2  45912  fsumnncl  46017  limcperiod  46073  sumnnodd  46075  limcresiooub  46085  limcresioolb  46086  0ellimcdiv  46092  reclimc  46096  limsupval3  46135  limsupequzmpt2  46161  liminfval5  46208  limsupresxr  46209  liminfresxr  46210  liminfvalxr  46226  liminfequzmpt2  46234  climliminflimsupd  46244  liminfltlem  46247  liminflbuz2  46258  sinmulcos  46308  coskpi2  46309  cncfdmsn  46333  cncfiooicclem1  46336  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  fperdvper  46362  dvnmptdivc  46381  dvnxpaek  46385  dvnmul  46386  dvnprodlem1  46389  dvnprodlem3  46391  itgcoscmulx  46412  itgsincmulx  46417  itgspltprt  46422  itgiccshift  46423  itgperiod  46424  sublevolico  46427  volioof  46430  ovolsplit  46431  fvvolioof  46432  fvvolicof  46434  stoweidlem22  46465  stoweidlem32  46475  wallispilem5  46512  stirlinglem5  46521  dirkertrigeqlem2  46542  dirkertrigeq  46544  dirkercncflem1  46546  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem13  46563  fourierdlem16  46566  fourierdlem19  46569  fourierdlem21  46571  fourierdlem22  46572  fourierdlem28  46578  fourierdlem32  46582  fourierdlem33  46583  fourierdlem42  46592  fourierdlem47  46596  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem56  46605  fourierdlem60  46609  fourierdlem61  46610  fourierdlem64  46613  fourierdlem66  46615  fourierdlem71  46620  fourierdlem73  46622  fourierdlem74  46623  fourierdlem76  46625  fourierdlem78  46627  fourierdlem79  46628  fourierdlem80  46629  fourierdlem81  46630  fourierdlem83  46632  fourierdlem88  46637  fourierdlem92  46641  fourierdlem93  46642  fourierdlem97  46646  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem109  46658  fourierdlem111  46660  fouriersw  46674  elaa2lem  46676  etransclem24  46701  etransclem25  46702  etransclem35  46712  etransclem46  46723  rrndistlt  46733  rrxunitopnfi  46735  qndenserrnbl  46738  qndenserrnopnlem  46740  saldifcl2  46771  intsal  46773  sge0sn  46822  sge0ltfirp  46843  sge0iunmptlemre  46858  sge0fodjrnlem  46859  sge0isum  46870  sge0xaddlem1  46876  nnfoctbdjlem  46898  meassle  46906  ismeannd  46910  meadif  46922  meaiuninclem  46923  meaiininclem  46929  omeunile  46948  caragendifcl  46957  caratheodory  46971  isomenndlem  46973  ovnsubaddlem1  47013  hoidmv1lelem2  47035  hoidmv1le  47037  hoidmvlelem2  47039  hoidmvle  47043  hoi2toco  47050  rrnmbl  47057  hoidifhspdmvle  47063  voncmpl  47064  hoiqssbl  47068  hspmbllem1  47069  hspmbllem2  47070  ovolval2lem  47086  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  hoimbl2  47108  vonhoire  47115  salpreimagelt  47150  salpreimalegt  47152  preimaioomnf  47162  smfres  47233  smfmullem1  47234  smflimmpt  47253  smfsupmpt  47258  smfinfmpt  47262  smflimsupmpt  47272  smfliminflem  47273  smfliminfmpt  47275  sigarcol  47307  sin5tlem2  47337  f1oresf1o  47753  elsprel  47950  prproropf1o  47982  paireqne  47986  sfprmdvdsmersenne  48081  lighneallem3  48085  lighneallem4  48088  nprmdvdsfacm1lem1  48098  nn0onn0exALTV  48190  nnsum3primesprm  48281  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  isuspgrim0lem  48384  clnbgrgrimlem  48424  uspgrlimlem3  48481  uspgrlimlem4  48482  gpgedgvtx0  48552  gpgedgvtx1  48553  funcringcsetcALTV2lem7  48787  funcringcsetclem7ALTV  48810  lincext3  48947  lincresunit3  48972  nn0onn0ex  49014  nnpw2pmod  49074  blennn0em1  49082  digexp  49098  dignn0ehalf  49108  nn0mulfsum  49115  itcovalpclem1  49161  eenglngeehlnmlem2  49229  rrx2vlinest  49232  line2  49243  itschlc0xyqsol  49258  itsclinecirc0b  49265  toplatjoin  49492  toplatmeet  49493  upeu2lem  49518  oppff1o  49639  imaf1co  49645  upciclem3  49658  natoppfb  49721  oppcthinco  49929  oppcthinendcALT  49931  lmddu  50157  recsec  50246  reccsc  50247  aacllem  50291  amgmlemALT  50293