Theorem eqtr2d 2796

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 2795	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2766	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 2155  ax-ext 2732

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

This theorem is used by:  3eqtrrd  2800  3eqtr2rd  2802  ifan  4536  ifor  4537  dfopif  4830  fnco  6650  fnsnfv  6957  nvocnv  7282  elovmpt3rab1  7674  onsucmin  7817  csbopeq1a  8047  oaabs2  8637  ecinxp  8792  resixpfo  8943  sbthlem3  9087  rankxpsuc  9864  fseqenlem2  10028  dfac2b  10133  isf32lem9  10363  compsscnvlem  10372  ttukeylem7  10517  fpwwe2lem10  10649  00id  11409  submul2  11678  mulsubfacd  11699  divadddiv  11954  infrenegsup  12222  xadd4d  13355  fzdifsuc  13639  fzval3  13790  fzoshftral  13843  ceim1l  13908  fldiv  13921  flmod  13946  intfrac  13947  modcyc2  13968  modaddb  13970  moddi  14003  uzrdgfni  14022  axdc4uzlem  14047  seqf1olem1  14105  seqf1olem2  14106  seqid2  14112  expnegz  14160  binom2sub  14284  binom3  14288  hashreshashfun  14504  ccatw2s1p2  14705  ccats1pfxeq  14783  pfxccatin12lem2  14800  pfxccatin12  14802  swrdccat3b  14809  swrdrevpfx  14838  cshweqrep  14892  2cshwcshw  14896  ccatco  14906  swrds2  15011  relexpsucnnr  15098  relexpaddnn  15124  sgnmul  15180  reim  15196  mulre  15208  addcj  15235  absimle  15396  clim2ser  15742  isercoll2  15756  serf0  15768  iseralt  15772  summolem3  15800  isumclim3  15845  mptfzshft  15864  fsumrev  15865  fsum2mul  15875  incexc  15926  isumsplit  15929  mertenslem1  15973  fprodrev  16064  iprodclim3  16087  binomfallfaclem2  16126  ef4p  16201  tanval3  16222  efival  16240  sinmul  16260  bitsinvp1  16539  sadaddlem  16556  bitsshft  16565  smu01lem  16575  dfgcd2  16636  lcmgcdlem  16696  lcm1  16700  lcmfass  16736  eulerthlem2  16873  hashgcdeq  16881  powm2modprm  16895  pythagtriplem16  16922  pczpre  16939  pcqdiv  16949  pcadd  16981  pcfac  16991  prmreclem5  17012  4sqlem10  17039  4sqlem19  17055  vdwapun  17066  vdwlem1  17073  ramcl  17121  setsstruct  17268  strfvd  17292  strfv2d  17293  xpsff1o  17653  xpsrnbas  17657  2oppccomf  17813  oppcepi  17828  sscfn1  17906  sscfn2  17907  invfuc  18066  funcestrcsetclem7  18234  funcsetcestrclem7  18249  gsumsplit1r  18789  grpinvssd  19140  grpinvval2  19146  cycsubggend  19333  pmtrdifwrdellem2  19609  psgnunilem1  19620  psgnuni  19626  pgp0  19723  sylow1lem1  19725  sylow3lem2  19755  efgredleme  19870  efgcpbllemb  19882  frgpuptinv  19898  frgpup3lem  19904  gexexlem  19979  cyggenod  20011  gsumval3eu  20031  gsumval3  20034  gsumzaddlem  20048  dprd2db  20172  ablsimpgfindlem1  20236  ringinvdv  20555  c0snmgmhm  20603  rngcifuestrc  20801  funcrngcsetc  20802  funcrngcsetcALT  20803  funcringcsetc  20836  lss1d  21147  pwssplit1  21243  rhmqusnsg  21488  rngqiprnglin  21505  znzrh2  21758  regsumsupp  21835  ipassr2  21860  dsmmfi  21951  frlmlss  21964  frlmip  21991  frlmlbs  22010  frlmup3  22013  islindf4  22051  mplcoe3  22254  subrgascl  22282  evlseu  22299  psdadd  22391  ply1sclid  22514  ply1chr  22531  evls1addd  22596  evls1muld  22597  evls1vsca  22598  evls1maprhm  22601  evls1maplmhm  22602  evls1maprnss  22603  evl1maprhm  22604  1marepvmarrepid  22797  madurid  22866  smadiadetlem3  22890  matunitlindflem1  22901  matunitlindflem2  22902  mat2pmatghm  22955  pmatcollpwscmatlem1  23014  pm2mpmhmlem2  23044  cpmadurid  23092  cpmidgsumm2pm  23094  cpmadugsumlemB  23099  cayhamlem2  23109  ntrval2  23276  ordtuni  23415  cnclima  23493  cmpsub  23625  ptbasfi  23807  txbasval  23832  pt1hmeo  24032  alexsubALTlem1  24273  trust  24455  ussid  24486  ressuss  24488  ressprdsds  24597  imasdsf1olem  24599  setsms  24706  tmsxms  24712  tmsxpsmopn  24763  subgnm  24859  tngnm  24877  tngngp2  24878  xrsxmet  25036  xrge0gsumle  25060  metdstri  25078  xrhmeo  25174  lebnumlem3  25191  pcorevlem  25254  pi1xfrcnvlem  25284  clmabs  25311  cvsmuleqdivd  25362  rrxip  25618  rrxds  25621  rrxdsfi  25639  minveclem4a  25658  pjthlem1  25665  divcncf  25675  ovolunlem1a  25724  mbfres2  25873  i1faddlem  25921  ibladdlem  26047  iblabs  26056  ditgsplit  26088  dvmptresicc  26143  dvnres  26158  dvmptdiv  26201  dveflem  26206  dveq0  26227  dvfsumabs  26250  itgsubstlem  26275  ply1divex  26362  r1pid2  26387  dgrco  26501  plycjlem  26502  taylthlem1  26609  pserdv2  26666  abelthlem6  26672  abelthlem7  26674  tangtx  26743  abssinper  26758  sineq0  26761  explog  26831  reexplog  26832  eflogeq  26839  abslogle  26855  tanarg  26856  logtayl  26897  logtayl2  26899  relogbdiv  27016  ang180lem3  27048  affineequiv  27060  affineequiv2  27061  chordthmlem4  27072  chordthmlem5  27073  heron  27075  dcubic1lem  27080  dcubic2  27081  dcubic  27083  mcubic  27084  cubic2  27085  dquartlem1  27088  dquart  27090  quart1lem  27092  quartlem1  27094  quart  27098  acoscos  27130  atanlogaddlem  27150  atantayl2  27175  atantayl3  27176  birthdaylem2  27189  efrlim  27206  amgmlem  27226  logdifbnd  27230  emcllem3  27234  emcllem6  27237  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamgulmlem4  27268  lgamgulmlem5  27269  gamigam  27289  lgamcvg2  27291  gamfac  27303  basellem3  27319  basellem8  27324  basellem9  27325  chtprm  27389  logfaclbnd  27458  perfect1  27464  bcp1ctr  27515  bclbnd  27516  bposlem1  27520  lgsdilem  27560  lgsdirnn0  27580  lgsdinn0  27581  gausslemma2dlem1a  27601  gausslemma2dlem4  27605  gausslemma2dlem5a  27606  lgseisenlem2  27612  lgsquadlem1  27616  2sqlem2  27654  mul2sq  27655  2sqmod  27672  2sqnn0  27674  vmadivsum  27718  rpvmasumlem  27723  dchrisumlem1  27725  dchrisumlem2  27726  dchrmusum2  27730  dchrvmasum2if  27733  dchrisum0lem2  27754  logsqvma2  27779  selberg3  27795  selberg4lem1  27796  pntrsumo1  27801  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem5  27817  pntibndlem2  27827  pntlemk  27842  pntlemo  27843  ostth2lem4  27872  ostth3  27874  subsfo  28330  negsval2  28331  ltonold  28526  noseqrdgfn  28571  n0fincut  28620  addhalfcut  28724  bdayfinbndlem1  28732  z12shalf  28745  tgbtwndiff  28848  tgifscgr  28850  trgcgrg  28857  motcgr3  28887  tgbtwnconn1lem1  28914  tgbtwnconn1lem2  28915  ismir  29010  miriso  29021  midexlem  29043  symquadprlnglem  29044  ragmir  29054  footexALT  29072  footexlem1  29073  footexlem2  29074  colperpexlem3  29087  mideulem2  29089  midex  29092  opphllem3  29104  midcgr  29164  lmiisolem  29180  prlngmid2  29318  quadcgrprlng  29323  brbtwn2  29362  colinearalglem4  29366  axsegconlem1  29374  axpaschlem  29397  axcontlem4  29424  axcontlem7  29427  axcontlem8  29428  ushgredgedgloop  29691  pfxwlk  30145  crctcshwlkn0lem6  30283  wwlknlsw  30315  wwlksnextwrd  30365  clwlkclwwlklem2a3  30464  clwlkclwwlk2  30473  clwwlkel  30516  clwwlkfo  30520  clwwlkext2edg  30526  eupth2eucrct  30697  numclwwlk2lem1lem  30822  numclwwlk1lem2fo  30838  numclwlk2lem2f  30857  grpoidinvlem2  30986  nvmtri  31152  cnnvm  31163  nvnd  31169  ipidsq  31191  ipnm  31192  ipipcj  31196  blocnilem  31285  ipasslem2  31313  dipsubdir  31329  hvaddsubval  31514  pjhthlem1  31872  pjspansn  32058  pjo  32152  unoplin  32401  adjadj  32417  hmoplin  32423  eigvec1  32443  lnopeqi  32489  nmcexi  32507  lnfnsubi  32527  riesz3i  32543  kbass6  32602  leoprf2  32608  leoprf  32609  pjnmopi  32629  mdslmd1lem1  32806  mdslmd1lem2  32807  superpos  32835  ifeq3da  33021  fgreu  33144  cocnvf1o  33200  resf1o  33201  quad3d  33220  fprodex01  33295  ccatws1f1o  33393  wrdt2ind  33395  mndlactfo  33467  mndractfo  33469  gsummpt2d  33489  gsummptp1  33497  xrge0tsmseq  33515  gsumwrd2dccatlem  33517  gsumwrd2dccat  33518  symgfcoeu  33522  wrdpmtrlast  33533  psgnfzto1stlem  33540  psgnfzto1st  33545  cycpm2tr  33559  cycpmco2lem6  33571  cycpmco2lem7  33572  subrgchr  33676  elrgspnlem1  33682  elrgspnlem3  33684  elrgspnsubrunlem1  33687  rloccring  33711  rhmdvd  33764  qusrn  33838  nsgqusf1olem3  33844  rhmquskerlem  33853  elrspunsn  33857  mxidlirredi  33874  qsdrngi  33897  1arithidomlem1  33945  1arithidomlem2  33946  evls1subd  33982  deg1prod  33993  0mplrim  34024  evlextv  34052  psrmonprod  34062  esplyfval1  34083  esplyind  34085  esplyindfv  34086  esplyfvn  34087  vietalem  34089  resssra  34097  dimval  34111  dimvalfi  34112  lindsunlem  34134  dimkerim  34137  qusdimsum  34138  fedgmullem1  34139  extdg1id  34176  fldextrspunlsplem  34183  fldextrspunlsp  34184  fldextrspunlem1  34185  fldextrspundgdvds  34191  extdgfialglem1  34202  extdgfialglem2  34203  ply1annidllem  34211  algextdeglem4  34230  constrrtcc  34245  constrsslem  34251  constrresqrtcl  34287  cos9thpiminplylem2  34293  cos9thpiminply  34298  madjusmdetlem2  34338  qtophaus  34346  zarclssn  34383  zarcmplem  34391  pstmval  34405  mndpluscn  34436  qqhucn  34502  esumval  34556  gsumesum  34569  esumcst  34573  esumpcvgval  34588  oddpwdc  34865  eulerpartlemgvv  34887  probdif  34931  signsvtn  35092  actfunsnf1o  35112  reprpmtf1o  35134  hgt750lemd  35156  logdivsqrle  35158  hgt750lemg  35162  hgt750lemb  35164  bnj1415  35547  vonf1oonfo  35712  derangen2  35753  subfaclefac  35755  subfaclim  35767  satom  35935  fmla  35960  mrsubrn  36092  sinccvglem  36251  bcprod  36317  nmulss1  36794  filnetlem4  37000  curunc  38356  ltflcei  38362  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem24  38393  mblfinlem4  38409  ibladdnclem  38425  iblabsnc  38433  iblmulc2nc  38434  ftc1anclem6  38447  ftc1anclem8  38449  sdclem2  38492  ismtycnv  38552  heiborlem10  38570  lflvsass  39954  lkrscss  39971  eqlkr  39972  eqlkr3  39974  ldualvsdi2  40017  omllaw3  40118  cmtcomlemN  40121  cmtbr3N  40127  omlfh3N  40132  llnexchb2lem  40741  dalawlem7  40750  dalawlem11  40754  dalawlem12  40755  pol1N  40783  paddatclN  40822  4atexlemcnd  40945  ltrncoidN  41001  cdleme3b  41102  cdleme11  41143  cdleme15a  41147  cdleme22e  41217  cdleme22g  41221  cdlemg18b  41552  trlcoat  41596  cdlemk2  41705  cdlemk4  41707  cdlemki  41714  cdlemksv2  41720  cdlemk15  41728  cdlemk55a  41832  diainN  41930  dia2dimlem3  41939  dia2dimlem5  41941  dvhlveclem  41981  diaocN  41998  cdlemn4  42071  cdlemn8  42077  dihopelvalcpre  42121  dihmeetlem9N  42188  dih1dimatlem  42202  dihpN  42209  dochvalr3  42236  dochsat  42256  djhjlj  42276  dochdmm1  42283  dihjatcclem4  42294  dihjat1  42302  dihjat4  42306  dochsnkr2cl  42347  dochfl1  42349  lclkrlem2j  42389  mapdordlem2  42510  mapdrvallem2  42518  hdmap10  42713  lcmineqlem12  42906  3lexlogpow5ineq5  42926  aks4d1p1  42942  primrootsunit1  42963  primrootscoprmpow  42965  posbezout  42966  aks6d1c1p3  42976  aks6d1c1p4  42977  aks6d1c1p5  42978  aks6d1c1p7  42979  evl1gprodd  42983  hashscontpow1  42987  aks6d1c3  42989  aks6d1c2lem3  42992  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c5lem3  43003  aks6d1c6lem1  43036  aks6d1c6isolem3  43042  aks6d1c6lem5  43043  bcle2d  43045  aks6d1c7lem1  43046  aks5lem3a  43055  grpods  43060  unitscyglem1  43061  unitscyglem2  43062  unitscyglem4  43064  unitscyglem5  43065  aks5lem7  43066  nicomachus  43187  sumcubes  43188  cnreeu  43378  frlmvscadiccat  43394  grpcominv1  43396  riccrng1  43403  ricdrng1  43410  frlmsnic  43422  evlselv  43435  fsuppind  43436  flt4lem7  43505  negexpidd  43527  3cubeslem2  43530  3cubeslem3r  43532  mzpsubmpt  43588  irrapxlem3  43665  pellexlem6  43675  pell1234qrne0  43694  pell1234qrreccl  43695  pell1234qrmulcl  43696  pell14qrdich  43710  pell1qrgaplem  43714  rmxluc  43777  rmyluc  43778  jm2.24nn  43800  jm2.18  43829  jm2.19lem2  43831  jm2.19lem3  43832  jm2.22  43836  jm2.23  43837  jm2.16nn0  43845  jm2.27c  43848  fnwe2lem2  43892  lmhmfgsplit  43927  hbtlem2  43965  onsucf1lem  44110  ofoafo  44197  naddcnffo  44205  naddwordnexlem4  44242  reabssgn  44476  relexpmulnn  44549  relexpmulg  44550  ntrclsneine0lem  44904  int-addassocd  45014  dvconstbi  45158  bccm1k  45166  binomcxplemnotnn0  45180  fmptsnxp  46001  wessf1ornlem  46017  projf1o  46028  infnsuprnmpt  46079  lefldiveq  46125  lt4addmuld  46139  fzdifsuc2  46143  suplesup  46169  infrpge  46181  xrlexaddrp  46182  xralrple2  46184  infleinflem1  46199  supminfrnmpt  46273  supminfxr2  46297  fsumnncl  46402  limcperiod  46458  sumnnodd  46460  limcresiooub  46470  limcresioolb  46471  0ellimcdiv  46477  reclimc  46481  limsupval3  46520  limsupequzmpt2  46546  liminfval5  46593  limsupresxr  46594  liminfresxr  46595  liminfvalxr  46611  liminfequzmpt2  46619  climliminflimsupd  46629  liminfltlem  46632  liminflbuz2  46643  sinmulcos  46693  coskpi2  46694  cncfdmsn  46718  cncfiooicclem1  46721  fprodsubrecnncnvlem  46735  fprodaddrecnncnvlem  46737  fperdvper  46747  dvnmptdivc  46766  dvnxpaek  46770  dvnmul  46771  dvnprodlem1  46774  dvnprodlem3  46776  itgcoscmulx  46797  itgsincmulx  46802  itgspltprt  46807  itgiccshift  46808  itgperiod  46809  sublevolico  46812  volioof  46815  ovolsplit  46816  fvvolioof  46817  fvvolicof  46819  stoweidlem22  46850  stoweidlem32  46860  wallispilem5  46897  stirlinglem5  46906  dirkertrigeqlem2  46927  dirkertrigeq  46929  dirkercncflem1  46931  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem13  46948  fourierdlem16  46951  fourierdlem19  46954  fourierdlem21  46956  fourierdlem22  46957  fourierdlem28  46963  fourierdlem32  46967  fourierdlem33  46968  fourierdlem42  46977  fourierdlem47  46981  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem56  46990  fourierdlem60  46994  fourierdlem61  46995  fourierdlem64  46998  fourierdlem66  47000  fourierdlem71  47005  fourierdlem73  47007  fourierdlem74  47008  fourierdlem76  47010  fourierdlem78  47012  fourierdlem79  47013  fourierdlem80  47014  fourierdlem81  47015  fourierdlem83  47017  fourierdlem88  47022  fourierdlem92  47026  fourierdlem93  47027  fourierdlem97  47031  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem109  47043  fourierdlem111  47045  fouriersw  47059  elaa2lem  47061  etransclem24  47086  etransclem25  47087  etransclem35  47097  etransclem46  47108  rrndistlt  47118  rrxunitopnfi  47120  qndenserrnbl  47123  qndenserrnopnlem  47125  saldifcl2  47156  intsal  47158  sge0sn  47207  sge0ltfirp  47228  sge0iunmptlemre  47243  sge0fodjrnlem  47244  sge0isum  47255  sge0xaddlem1  47261  nnfoctbdjlem  47283  meassle  47291  ismeannd  47295  meadif  47307  meaiuninclem  47308  meaiininclem  47314  omeunile  47333  caragendifcl  47342  caratheodory  47356  isomenndlem  47358  ovnsubaddlem1  47398  hoidmv1lelem2  47420  hoidmv1le  47422  hoidmvlelem2  47424  hoidmvle  47428  hoi2toco  47435  rrnmbl  47442  hoidifhspdmvle  47448  voncmpl  47449  hoiqssbl  47453  hspmbllem1  47454  hspmbllem2  47455  ovolval2lem  47471  ovolval5lem2  47481  ovnovollem1  47484  ovnovollem2  47485  hoimbl2  47493  vonhoire  47500  salpreimagelt  47535  salpreimalegt  47537  preimaioomnf  47547  smfres  47618  smfmullem1  47619  smflimmpt  47638  smfsupmpt  47643  smfinfmpt  47647  smflimsupmpt  47657  smfliminflem  47658  smfliminfmpt  47660  sigarcol  47692  sin5tlem2  47738  sinnpoly  47759  sqrtnpoly  47761  f1oresf1o  48178  elsprel  48375  prproropf1o  48407  paireqne  48411  sfprmdvdsmersenne  48506  lighneallem3  48510  lighneallem4  48513  nprmdvdsfacm1lem1  48523  nn0onn0exALTV  48615  nnsum3primesprm  48706  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  isuspgrim0lem  48809  clnbgrgrimlem  48849  uspgrlimlem3  48906  uspgrlimlem4  48907  gpgedgvtx0  48977  gpgedgvtx1  48978  funcringcsetcALTV2lem7  49211  funcringcsetclem7ALTV  49234  lincext3  49386  lincresunit3  49411  nn0onn0ex  49453  nnpw2pmod  49513  blennn0em1  49521  digexp  49537  dignn0ehalf  49547  nn0mulfsum  49554  itcovalpclem1  49600  eenglngeehlnmlem2  49668  rrx2vlinest  49671  line2  49682  itschlc0xyqsol  49697  itsclinecirc0b  49704  toplatjoin  49928  toplatmeet  49929  upeu2lem  49954  oppff1o  50075  imaf1co  50081  upciclem3  50094  natoppfb  50157  oppcthinco  50365  oppcthinendcALT  50367  lmddu  50593  recsec  50682  reccsc  50683  aacllem  50772  crossp3d  50800  amgmlemALT  50821