Theorem eqtr2d 2805

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  3eqtrrd  2809  3eqtr2rd  2811  ifan  4543  ifor  4544  dfopif  4836  fnco  6651  fnsnfv  6958  nvocnv  7277  elovmpt3rab1  7668  onsucmin  7813  csbopeq1a  8043  oaabs2  8631  ecinxp  8786  resixpfo  8930  sbthlem3  9073  rankxpsuc  9850  fseqenlem2  10005  dfac2b  10110  isf32lem9  10341  compsscnvlem  10350  ttukeylem7  10495  fpwwe2lem10  10621  00id  11381  submul2  11650  mulsubfacd  11671  divadddiv  11926  infrenegsup  12194  xadd4d  13325  fzdifsuc  13608  fzval3  13759  fzoshftral  13812  ceim1l  13876  fldiv  13889  flmod  13914  intfrac  13915  modcyc2  13936  modaddb  13938  moddi  13971  uzrdgfni  13990  axdc4uzlem  14015  seqf1olem1  14073  seqf1olem2  14074  seqid2  14080  expnegz  14128  binom2sub  14252  binom3  14256  hashreshashfun  14472  ccatw2s1p2  14671  ccats1pfxeq  14747  pfxccatin12lem2  14764  pfxccatin12  14766  swrdccat3b  14773  cshweqrep  14854  2cshwcshw  14858  ccatco  14868  swrds2  14973  relexpsucnnr  15058  relexpaddnn  15084  sgnmul  15140  reim  15156  mulre  15168  addcj  15195  absimle  15356  clim2ser  15702  isercoll2  15716  serf0  15728  iseralt  15732  summolem3  15761  isumclim3  15806  mptfzshft  15825  fsumrev  15826  fsum2mul  15836  incexc  15887  isumsplit  15890  mertenslem1  15934  fprodrev  16027  iprodclim3  16050  binomfallfaclem2  16090  ef4p  16165  tanval3  16186  efival  16204  sinmul  16224  bitsinvp1  16503  sadaddlem  16520  bitsshft  16529  smu01lem  16539  dfgcd2  16600  lcmgcdlem  16660  lcm1  16664  lcmfass  16700  eulerthlem2  16837  hashgcdeq  16845  powm2modprm  16859  pythagtriplem16  16886  pczpre  16903  pcqdiv  16913  pcadd  16945  pcfac  16955  prmreclem5  16976  4sqlem10  17003  4sqlem19  17019  vdwapun  17030  vdwlem1  17037  ramcl  17085  setsstruct  17232  strfvd  17256  strfv2d  17257  xpsff1o  17617  xpsrnbas  17621  2oppccomf  17777  oppcepi  17792  sscfn1  17870  sscfn2  17871  invfuc  18030  funcestrcsetclem7  18198  funcsetcestrclem7  18213  gsumsplit1r  18741  grpinvssd  19079  grpinvval2  19085  cycsubggend  19272  pmtrdifwrdellem2  19548  psgnunilem1  19559  psgnuni  19565  pgp0  19662  sylow1lem1  19664  sylow3lem2  19694  efgredleme  19809  efgcpbllemb  19821  frgpuptinv  19837  frgpup3lem  19843  gexexlem  19918  cyggenod  19950  gsumval3eu  19970  gsumval3  19973  gsumzaddlem  19987  dprd2db  20111  ablsimpgfindlem1  20175  ringinvdv  20492  c0snmgmhm  20540  rngcifuestrc  20720  funcrngcsetc  20721  funcrngcsetcALT  20722  funcringcsetc  20755  lss1d  21058  pwssplit1  21154  rhmqusnsg  21392  rngqiprnglin  21409  znzrh2  21660  regsumsupp  21737  ipassr2  21762  dsmmfi  21853  frlmlss  21866  frlmip  21893  frlmlbs  21912  frlmup3  21915  islindf4  21953  mplcoe3  22154  subrgascl  22182  evlseu  22199  psdadd  22291  ply1sclid  22414  ply1chr  22431  evls1addd  22496  evls1muld  22497  evls1vsca  22498  evls1maprhm  22501  evls1maplmhm  22502  evls1maprnss  22503  evl1maprhm  22504  1marepvmarrepid  22697  madurid  22766  smadiadetlem3  22790  mat2pmatghm  22852  pmatcollpwscmatlem1  22911  pm2mpmhmlem2  22941  cpmadurid  22989  cpmidgsumm2pm  22991  cpmadugsumlemB  22996  cayhamlem2  23006  ntrval2  23173  ordtuni  23312  cnclima  23390  cmpsub  23522  ptbasfi  23703  txbasval  23728  pt1hmeo  23928  alexsubALTlem1  24169  trust  24351  ussid  24382  ressuss  24384  ressprdsds  24493  imasdsf1olem  24495  setsms  24602  tmsxms  24608  tmsxpsmopn  24659  subgnm  24755  tngnm  24773  tngngp2  24774  xrsxmet  24932  xrge0gsumle  24956  metdstri  24974  xrhmeo  25070  lebnumlem3  25087  pcorevlem  25150  pi1xfrcnvlem  25180  clmabs  25207  cvsmuleqdivd  25258  rrxip  25514  rrxds  25517  rrxdsfi  25535  minveclem4a  25554  pjthlem1  25561  divcncf  25571  ovolunlem1a  25620  mbfres2  25769  i1faddlem  25817  ibladdlem  25944  iblabs  25953  ditgsplit  25985  dvmptresicc  26040  dvnres  26055  dvmptdiv  26098  dveflem  26103  dveq0  26124  dvfsumabs  26147  itgsubstlem  26172  ply1divex  26259  r1pid2  26284  dgrco  26397  plycjlem  26398  taylthlem1  26498  pserdv2  26555  abelthlem6  26561  abelthlem7  26563  tangtx  26632  abssinper  26648  sineq0  26651  explog  26721  reexplog  26722  eflogeq  26729  abslogle  26745  tanarg  26746  logtayl  26787  logtayl2  26789  relogbdiv  26906  ang180lem3  26938  affineequiv  26950  affineequiv2  26951  chordthmlem4  26962  chordthmlem5  26963  heron  26965  dcubic1lem  26970  dcubic2  26971  dcubic  26973  mcubic  26974  cubic2  26975  dquartlem1  26978  dquart  26980  quart1lem  26982  quartlem1  26984  quart  26988  acoscos  27020  atanlogaddlem  27040  atantayl2  27065  atantayl3  27066  birthdaylem2  27079  efrlim  27096  amgmlem  27116  logdifbnd  27120  emcllem3  27124  emcllem6  27127  lgamgulmlem2  27156  lgamgulmlem3  27157  lgamgulmlem4  27158  lgamgulmlem5  27159  gamigam  27179  lgamcvg2  27181  gamfac  27193  basellem3  27209  basellem8  27214  basellem9  27215  chtprm  27279  logfaclbnd  27348  perfect1  27354  bcp1ctr  27405  bclbnd  27406  bposlem1  27410  lgsdilem  27450  lgsdirnn0  27470  lgsdinn0  27471  gausslemma2dlem1a  27491  gausslemma2dlem4  27495  gausslemma2dlem5a  27496  lgseisenlem2  27502  lgsquadlem1  27506  2sqlem2  27544  mul2sq  27545  2sqmod  27562  2sqnn0  27564  vmadivsum  27608  rpvmasumlem  27613  dchrisumlem1  27615  dchrisumlem2  27616  dchrmusum2  27620  dchrvmasum2if  27623  dchrisum0lem2  27644  logsqvma2  27669  selberg3  27685  selberg4lem1  27686  pntrsumo1  27691  pntrlog2bndlem2  27704  pntrlog2bndlem3  27705  pntrlog2bndlem5  27707  pntibndlem2  27717  pntlemk  27732  pntlemo  27733  ostth2lem4  27762  ostth3  27764  subsfo  28220  negsval2  28221  ltonold  28416  noseqrdgfn  28461  n0fincut  28510  addhalfcut  28614  bdayfinbndlem1  28622  z12shalf  28635  tgbtwndiff  28737  tgifscgr  28739  trgcgrg  28746  motcgr3  28776  tgbtwnconn1lem1  28803  tgbtwnconn1lem2  28804  ismir  28894  miriso  28905  midexlem  28927  ragmir  28935  footexALT  28953  footexlem1  28954  footexlem2  28955  colperpexlem3  28968  mideulem2  28970  midex  28973  opphllem3  28985  midcgr  29043  lmiisolem  29059  brbtwn2  29192  colinearalglem4  29196  axsegconlem1  29204  axpaschlem  29227  axcontlem4  29254  axcontlem7  29257  axcontlem8  29258  ushgredgedgloop  29518  crctcshwlkn0lem6  30101  wwlknlsw  30133  wwlksnextwrd  30183  clwlkclwwlklem2a3  30282  clwlkclwwlk2  30291  clwwlkel  30334  clwwlkfo  30338  clwwlkext2edg  30344  eupth2eucrct  30505  numclwwlk2lem1lem  30630  numclwwlk1lem2fo  30646  numclwlk2lem2f  30665  grpoidinvlem2  30794  nvmtri  30960  cnnvm  30971  nvnd  30977  ipidsq  30999  ipnm  31000  ipipcj  31004  blocnilem  31093  ipasslem2  31121  dipsubdir  31137  hvaddsubval  31322  pjhthlem1  31680  pjspansn  31866  pjo  31960  unoplin  32209  adjadj  32225  hmoplin  32231  eigvec1  32251  lnopeqi  32297  nmcexi  32315  lnfnsubi  32335  riesz3i  32351  kbass6  32410  leoprf2  32416  leoprf  32417  pjnmopi  32437  mdslmd1lem1  32614  mdslmd1lem2  32615  superpos  32643  ifeq3da  32829  fgreu  32953  cocnvf1o  33011  resf1o  33012  quad3d  33031  fprodex01  33106  ccatws1f1o  33208  wrdt2ind  33210  mndlactfo  33284  mndractfo  33286  gsummpt2d  33306  gsummptp1  33314  xrge0tsmseq  33332  gsumwrd2dccatlem  33334  gsumwrd2dccat  33335  symgfcoeu  33339  wrdpmtrlast  33350  psgnfzto1stlem  33357  psgnfzto1st  33362  cycpm2tr  33376  cycpmco2lem6  33388  cycpmco2lem7  33389  subrgchr  33493  elrgspnlem1  33499  elrgspnlem3  33501  elrgspnsubrunlem1  33504  rloccring  33528  rhmdvd  33583  qusrn  33658  nsgqusf1olem3  33664  rhmquskerlem  33673  elrspunsn  33677  mxidlirredi  33695  qsdrngi  33718  1arithidomlem1  33766  1arithidomlem2  33767  evls1subd  33803  deg1prod  33814  0mplrim  33845  evlextv  33873  psrmonprod  33883  esplyfval1  33904  esplyind  33906  esplyindfv  33907  esplyfvn  33908  vietalem  33910  resssra  33918  dimval  33932  dimvalfi  33933  lindsunlem  33955  dimkerim  33958  qusdimsum  33959  fedgmullem1  33960  extdg1id  33997  fldextrspunlsplem  34004  fldextrspunlsp  34005  fldextrspunlem1  34006  fldextrspundgdvds  34012  extdgfialglem1  34023  extdgfialglem2  34024  ply1annidllem  34032  algextdeglem4  34051  constrrtcc  34066  constrsslem  34072  constrresqrtcl  34108  cos9thpiminplylem2  34114  cos9thpiminply  34119  madjusmdetlem2  34159  qtophaus  34167  zarclssn  34204  zarcmplem  34212  pstmval  34226  mndpluscn  34257  qqhucn  34323  esumval  34377  gsumesum  34390  esumcst  34394  esumpcvgval  34409  oddpwdc  34685  eulerpartlemgvv  34707  probdif  34751  signsvtn  34912  actfunsnf1o  34932  reprpmtf1o  34954  hgt750lemd  34976  logdivsqrle  34978  hgt750lemg  34982  hgt750lemb  34984  bnj1415  35367  vonf1oonfo  35494  swrdrevpfx  35503  pfxwlk  35511  derangen2  35561  subfaclefac  35563  subfaclim  35575  satom  35743  fmla  35768  mrsubrn  35900  sinccvglem  36059  bcprod  36125  filnetlem4  36777  curunc  38136  ltflcei  38142  matunitlindflem1  38150  matunitlindflem2  38151  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem24  38178  mblfinlem4  38194  ibladdnclem  38210  iblabsnc  38218  iblmulc2nc  38219  ftc1anclem6  38232  ftc1anclem8  38234  sdclem2  38276  ismtycnv  38336  heiborlem10  38354  lflvsass  39740  lkrscss  39757  eqlkr  39758  eqlkr3  39760  ldualvsdi2  39803  omllaw3  39904  cmtcomlemN  39907  cmtbr3N  39913  omlfh3N  39918  llnexchb2lem  40527  dalawlem7  40536  dalawlem11  40540  dalawlem12  40541  pol1N  40569  paddatclN  40608  4atexlemcnd  40731  ltrncoidN  40787  cdleme3b  40888  cdleme11  40929  cdleme15a  40933  cdleme22e  41003  cdleme22g  41007  cdlemg18b  41338  trlcoat  41382  cdlemk2  41491  cdlemk4  41493  cdlemki  41500  cdlemksv2  41506  cdlemk15  41514  cdlemk55a  41618  diainN  41716  dia2dimlem3  41725  dia2dimlem5  41727  dvhlveclem  41767  diaocN  41784  cdlemn4  41857  cdlemn8  41863  dihopelvalcpre  41907  dihmeetlem9N  41974  dih1dimatlem  41988  dihpN  41995  dochvalr3  42022  dochsat  42042  djhjlj  42062  dochdmm1  42069  dihjatcclem4  42080  dihjat1  42088  dihjat4  42092  dochsnkr2cl  42133  dochfl1  42135  lclkrlem2j  42175  mapdordlem2  42296  mapdrvallem2  42304  hdmap10  42499  lcmineqlem12  42692  3lexlogpow5ineq5  42712  aks4d1p1  42728  primrootsunit1  42749  primrootscoprmpow  42751  posbezout  42752  aks6d1c1p3  42762  aks6d1c1p4  42763  aks6d1c1p5  42764  aks6d1c1p7  42765  evl1gprodd  42769  hashscontpow1  42773  aks6d1c3  42775  aks6d1c2lem3  42778  aks6d1c2lem4  42779  aks6d1c2  42782  aks6d1c5lem3  42789  aks6d1c6lem1  42822  aks6d1c6isolem3  42828  aks6d1c6lem5  42829  bcle2d  42831  aks6d1c7lem1  42832  aks5lem3a  42841  grpods  42846  unitscyglem1  42847  unitscyglem2  42848  unitscyglem4  42850  unitscyglem5  42851  aks5lem7  42852  nicomachus  42958  sumcubes  42959  cnreeu  43149  frlmvscadiccat  43165  grpcominv1  43167  riccrng1  43176  ricdrng1  43183  frlmsnic  43195  evlselv  43208  fsuppind  43209  flt4lem7  43278  negexpidd  43300  3cubeslem2  43303  3cubeslem3r  43305  mzpsubmpt  43361  irrapxlem3  43438  pellexlem6  43448  pell1234qrne0  43467  pell1234qrreccl  43468  pell1234qrmulcl  43469  pell14qrdich  43483  pell1qrgaplem  43487  rmxluc  43550  rmyluc  43551  jm2.24nn  43573  jm2.18  43602  jm2.19lem2  43604  jm2.19lem3  43605  jm2.22  43609  jm2.23  43610  jm2.16nn0  43618  jm2.27c  43621  fnwe2lem2  43665  lmhmfgsplit  43700  hbtlem2  43738  onsucf1lem  43883  ofoafo  43970  naddcnffo  43978  naddwordnexlem4  44015  reabssgn  44249  relexpmulnn  44322  relexpmulg  44323  ntrclsneine0lem  44677  int-addassocd  44787  dvconstbi  44931  bccm1k  44939  binomcxplemnotnn0  44953  fmptsnxp  45774  wessf1ornlem  45790  projf1o  45801  infnsuprnmpt  45852  lefldiveq  45898  lt4addmuld  45912  fzdifsuc2  45916  suplesup  45942  infrpge  45954  xrlexaddrp  45955  xralrple2  45957  infleinflem1  45972  supminfrnmpt  46046  supminfxr2  46070  fsumnncl  46175  limcperiod  46231  sumnnodd  46233  limcresiooub  46243  limcresioolb  46244  0ellimcdiv  46250  reclimc  46254  limsupval3  46293  limsupequzmpt2  46319  liminfval5  46366  limsupresxr  46367  liminfresxr  46368  liminfvalxr  46384  liminfequzmpt2  46392  climliminflimsupd  46402  liminfltlem  46405  liminflbuz2  46416  sinmulcos  46466  coskpi2  46467  cncfdmsn  46491  cncfiooicclem1  46494  fprodsubrecnncnvlem  46508  fprodaddrecnncnvlem  46510  fperdvper  46520  dvnmptdivc  46539  dvnxpaek  46543  dvnmul  46544  dvnprodlem1  46547  dvnprodlem3  46549  itgcoscmulx  46570  itgsincmulx  46575  itgspltprt  46580  itgiccshift  46581  itgperiod  46582  sublevolico  46585  volioof  46588  ovolsplit  46589  fvvolioof  46590  fvvolicof  46592  stoweidlem22  46623  stoweidlem32  46633  wallispilem5  46670  stirlinglem5  46679  dirkertrigeqlem2  46700  dirkertrigeq  46702  dirkercncflem1  46704  dirkercncflem2  46705  dirkercncflem4  46707  fourierdlem13  46721  fourierdlem16  46724  fourierdlem19  46727  fourierdlem21  46729  fourierdlem22  46730  fourierdlem28  46736  fourierdlem32  46740  fourierdlem33  46741  fourierdlem42  46750  fourierdlem47  46754  fourierdlem48  46755  fourierdlem49  46756  fourierdlem50  46757  fourierdlem56  46763  fourierdlem60  46767  fourierdlem61  46768  fourierdlem64  46771  fourierdlem66  46773  fourierdlem71  46778  fourierdlem73  46780  fourierdlem74  46781  fourierdlem76  46783  fourierdlem78  46785  fourierdlem79  46786  fourierdlem80  46787  fourierdlem81  46788  fourierdlem83  46790  fourierdlem88  46795  fourierdlem92  46799  fourierdlem93  46800  fourierdlem97  46804  fourierdlem101  46808  fourierdlem103  46810  fourierdlem104  46811  fourierdlem109  46816  fourierdlem111  46818  fouriersw  46832  elaa2lem  46834  etransclem24  46859  etransclem25  46860  etransclem35  46870  etransclem46  46881  rrndistlt  46891  rrxunitopnfi  46893  qndenserrnbl  46896  qndenserrnopnlem  46898  saldifcl2  46929  intsal  46931  sge0sn  46980  sge0ltfirp  47001  sge0iunmptlemre  47016  sge0fodjrnlem  47017  sge0isum  47028  sge0xaddlem1  47034  nnfoctbdjlem  47056  meassle  47064  ismeannd  47068  meadif  47080  meaiuninclem  47081  meaiininclem  47087  omeunile  47106  caragendifcl  47115  caratheodory  47129  isomenndlem  47131  ovnsubaddlem1  47171  hoidmv1lelem2  47193  hoidmv1le  47195  hoidmvlelem2  47197  hoidmvle  47201  hoi2toco  47208  rrnmbl  47215  hoidifhspdmvle  47221  voncmpl  47222  hoiqssbl  47226  hspmbllem1  47227  hspmbllem2  47228  ovolval2lem  47244  ovolval5lem2  47254  ovnovollem1  47257  ovnovollem2  47258  hoimbl2  47266  vonhoire  47273  salpreimagelt  47308  salpreimalegt  47310  preimaioomnf  47320  smfres  47391  smfmullem1  47392  smflimmpt  47411  smfsupmpt  47416  smfinfmpt  47420  smflimsupmpt  47430  smfliminflem  47431  smfliminfmpt  47433  sigarcol  47465  sin5tlem2  47495  f1oresf1o  47911  elsprel  48108  prproropf1o  48140  paireqne  48144  sfprmdvdsmersenne  48239  lighneallem3  48243  lighneallem4  48246  nprmdvdsfacm1lem1  48256  nn0onn0exALTV  48348  nnsum3primesprm  48439  nnsum4primesodd  48445  nnsum4primesoddALTV  48446  isuspgrim0lem  48542  clnbgrgrimlem  48582  uspgrlimlem3  48639  uspgrlimlem4  48640  gpgedgvtx0  48710  gpgedgvtx1  48711  funcringcsetcALTV2lem7  48945  funcringcsetclem7ALTV  48968  lincext3  49116  lincresunit3  49141  nn0onn0ex  49183  nnpw2pmod  49243  blennn0em1  49251  digexp  49267  dignn0ehalf  49277  nn0mulfsum  49284  itcovalpclem1  49330  eenglngeehlnmlem2  49398  rrx2vlinest  49401  line2  49412  itschlc0xyqsol  49427  itsclinecirc0b  49434  toplatjoin  49660  toplatmeet  49661  upeu2lem  49686  oppff1o  49807  imaf1co  49813  upciclem3  49826  natoppfb  49889  oppcthinco  50097  oppcthinendcALT  50099  lmddu  50325  recsec  50414  reccsc  50415  aacllem  50470  amgmlemALT  50472