Theorem eqtr2d 2857

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

Syntax hints:   → wi 4   = wceq 1537

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 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  3eqtrrd  2861  3eqtr2rd  2863  ifan  4518  ifor  4519  dfopif  4800  nvocnv  7038  elovmpt3rab1  7405  onsucmin  7536  csbopeq1a  7749  oaabs2  8272  ecinxp  8372  resixpfo  8500  sbthlem3  8629  rankxpsuc  9311  fseqenlem2  9451  dfac2b  9556  isf32lem9  9783  compsscnvlem  9792  ttukeylem7  9937  fpwwe2lem11  10062  00id  10815  submul2  11080  mulsubfacd  11101  divadddiv  11355  infrenegsup  11624  xadd4d  12697  fzdifsuc  12968  fzval3  13107  fzoshftral  13155  ceim1l  13216  fldiv  13229  flmod  13254  intfrac  13255  modcyc2  13276  moddi  13308  uzrdgfni  13327  axdc4uzlem  13352  seqf1olem1  13410  seqf1olem2  13411  seqid2  13417  expnegz  13464  binom2sub  13582  binom3  13586  hashreshashfun  13801  ccatw2s1p2  13997  ccats1pfxeq  14076  pfxccatin12lem2  14093  pfxccatin12  14095  swrdccat3b  14102  cshweqrep  14183  2cshwcshw  14187  ccatco  14197  swrds2  14302  relexpsucnnr  14384  relexpaddnn  14410  reim  14468  mulre  14480  addcj  14507  absimle  14669  clim2ser  15011  isercoll2  15025  serf0  15037  iseralt  15041  summolem3  15071  isumclim3  15114  mptfzshft  15133  fsumrev  15134  fsum2mul  15144  incexc  15192  isumsplit  15195  mertenslem1  15240  fprodrev  15331  iprodclim3  15354  binomfallfaclem2  15394  ef4p  15466  tanval3  15487  efival  15505  sinmul  15525  bitsinvp1  15798  sadaddlem  15815  bitsshft  15824  smu01lem  15834  dfgcd2  15894  lcmgcdlem  15950  lcm1  15954  lcmfass  15990  eulerthlem2  16119  hashgcdeq  16126  powm2modprm  16140  pythagtriplem16  16167  pczpre  16184  pcqdiv  16194  pcadd  16225  pcfac  16235  prmreclem5  16256  4sqlem10  16283  4sqlem19  16299  vdwapun  16310  vdwlem1  16317  ramcl  16365  setsstruct  16523  strfvd  16528  strfv2d  16529  xpsff1o  16840  xpsrnbas  16844  2oppccomf  16995  oppcepi  17009  sscfn1  17087  sscfn2  17088  invfuc  17244  funcestrcsetclem7  17396  funcsetcestrclem7  17411  gsumsplit1r  17897  grpinvssd  18176  grpinvval2  18182  cycsubggend  18348  pmtrdifwrdellem2  18610  psgnunilem1  18621  psgnuni  18627  pgp0  18721  sylow1lem1  18723  sylow3lem2  18753  efgredleme  18869  efgcpbllemb  18881  frgpuptinv  18897  frgpup3lem  18903  gexexlem  18972  cyggenod  19003  gsumval3eu  19024  gsumval3  19027  gsumzaddlem  19041  dprd2db  19165  ablsimpgfindlem1  19229  ringinvdv  19444  lss1d  19735  pwssplit1  19831  mplcoe3  20247  subrgascl  20278  evlseu  20296  mhpinvcl  20339  ply1sclid  20456  znzrh2  20692  regsumsupp  20766  ipassr2  20791  dsmmfi  20882  frlmlss  20895  frlmip  20922  frlmlbs  20941  frlmup3  20944  islindf4  20982  1marepvmarrepid  21184  madurid  21253  smadiadetlem3  21277  mat2pmatghm  21338  pmatcollpwscmatlem1  21397  pm2mpmhmlem2  21427  cpmadurid  21475  cpmidgsumm2pm  21477  cpmadugsumlemB  21482  cayhamlem2  21492  ntrval2  21659  ordtuni  21798  cnclima  21876  cmpsub  22008  ptbasfi  22189  txbasval  22214  pt1hmeo  22414  alexsubALTlem1  22655  trust  22838  ussid  22869  ressuss  22872  ressprdsds  22981  imasdsf1olem  22983  setsms  23090  tmsxms  23096  tmsxpsmopn  23147  subgnm  23242  tngnm  23260  tngngp2  23261  xrsxmet  23417  xrge0gsumle  23441  metdstri  23459  xrhmeo  23550  lebnumlem3  23567  pcorevlem  23630  pi1xfrcnvlem  23660  clmabs  23687  cvsmuleqdivd  23738  rrxip  23993  rrxds  23996  rrxdsfi  24014  minveclem4a  24033  pjthlem1  24040  divcncf  24048  ovolunlem1a  24097  mbfres2  24246  i1faddlem  24294  ibladdlem  24420  iblabs  24429  ditgsplit  24459  dvnres  24528  dvmptdiv  24571  dveflem  24576  dveq0  24597  dvfsumabs  24620  itgsubstlem  24645  ply1divex  24730  dgrco  24865  plycjlem  24866  taylthlem1  24961  pserdv2  25018  abelthlem6  25024  abelthlem7  25026  tangtx  25091  abssinper  25106  sineq0  25109  explog  25177  reexplog  25178  eflogeq  25185  abslogle  25201  tanarg  25202  logtayl  25243  logtayl2  25245  relogbdiv  25357  ang180lem3  25389  affineequiv  25401  affineequiv2  25402  chordthmlem4  25413  chordthmlem5  25414  heron  25416  dcubic1lem  25421  dcubic2  25422  dcubic  25424  mcubic  25425  cubic2  25426  dquartlem1  25429  dquart  25431  quart1lem  25433  quartlem1  25435  quart  25439  acoscos  25471  atanlogaddlem  25491  atantayl2  25516  atantayl3  25517  birthdaylem2  25530  efrlim  25547  amgmlem  25567  logdifbnd  25571  emcllem3  25575  emcllem6  25578  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  gamigam  25630  lgamcvg2  25632  gamfac  25644  basellem3  25660  basellem8  25665  basellem9  25666  chtprm  25730  logfaclbnd  25798  perfect1  25804  bcp1ctr  25855  bclbnd  25856  bposlem1  25860  lgsdilem  25900  lgsdirnn0  25920  lgsdinn0  25921  gausslemma2dlem1a  25941  gausslemma2dlem4  25945  gausslemma2dlem5a  25946  lgseisenlem2  25952  lgsquadlem1  25956  2sqlem2  25994  mul2sq  25995  2sqmod  26012  2sqnn0  26014  vmadivsum  26058  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem2  26066  dchrmusum2  26070  dchrvmasum2if  26073  dchrisum0lem2  26094  logsqvma2  26119  selberg3  26135  selberg4lem1  26136  pntrsumo1  26141  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntibndlem2  26167  pntlemk  26182  pntlemo  26183  ostth2lem4  26212  ostth3  26214  tgbtwndiff  26292  tgifscgr  26294  trgcgrg  26301  motcgr3  26331  tgbtwnconn1lem1  26358  tgbtwnconn1lem2  26359  ismir  26445  miriso  26456  midexlem  26478  ragmir  26486  footexALT  26504  footexlem1  26505  footexlem2  26506  colperpexlem3  26518  mideulem2  26520  midex  26523  opphllem3  26535  midcgr  26566  lmiisolem  26582  brbtwn2  26691  colinearalglem4  26695  axsegconlem1  26703  axpaschlem  26726  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  ushgredgedgloop  27013  crctcshwlkn0lem6  27593  wwlknlsw  27625  wwlksnextwrd  27675  clwlkclwwlklem2a3  27772  clwlkclwwlk2  27781  clwwlkel  27825  clwwlkfo  27829  clwwlkext2edg  27835  eupth2eucrct  27996  numclwwlk2lem1lem  28121  numclwwlk1lem2fo  28137  numclwlk2lem2f  28156  grpoidinvlem2  28282  nvmtri  28448  cnnvm  28459  nvnd  28465  ipidsq  28487  ipnm  28488  ipipcj  28492  blocnilem  28581  ipasslem2  28609  dipsubdir  28625  hvaddsubval  28810  pjhthlem1  29168  pjspansn  29354  pjo  29448  unoplin  29697  adjadj  29713  hmoplin  29719  eigvec1  29739  lnopeqi  29785  nmcexi  29803  lnfnsubi  29823  riesz3i  29839  kbass6  29898  leoprf2  29904  leoprf  29905  pjnmopi  29925  mdslmd1lem1  30102  mdslmd1lem2  30103  superpos  30131  ifeq3da  30301  fgreu  30417  resf1o  30466  fprodex01  30541  wrdt2ind  30627  gsummpt2d  30687  xrge0tsmseq  30694  symgfcoeu  30726  psgnfzto1stlem  30742  psgnfzto1st  30747  cycpm2tr  30761  cycpmco2lem6  30773  cycpmco2lem7  30774  subrgchr  30865  rhmdvd  30894  dimval  31001  dimvalfi  31002  lindsunlem  31020  dimkerim  31023  qusdimsum  31024  fedgmullem1  31025  fedgmullem2  31026  extdg1id  31053  madjusmdetlem2  31093  qtophaus  31100  pstmval  31135  mndpluscn  31169  qqhucn  31233  esumval  31305  gsumesum  31318  esumcst  31322  esumpcvgval  31337  oddpwdc  31612  eulerpartlemgvv  31634  probdif  31678  sgnmul  31800  signsvtn  31854  actfunsnf1o  31875  reprpmtf1o  31897  hgt750lemd  31919  logdivsqrle  31921  hgt750lemg  31925  hgt750lemb  31927  bnj1415  32310  swrdrevpfx  32363  pfxwlk  32370  derangen2  32421  subfaclefac  32423  subfaclim  32435  satom  32603  fmla  32628  mrsubrn  32760  sinccvglem  32915  bcprod  32970  filnetlem4  33729  curunc  34889  ltflcei  34895  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem24  34931  mblfinlem4  34947  ibladdnclem  34963  iblabsnc  34971  iblmulc2nc  34972  ftc1anclem6  34987  ftc1anclem8  34989  sdclem2  35032  ismtycnv  35095  heiborlem10  35113  lflvsass  36232  lkrscss  36249  eqlkr  36250  eqlkr3  36252  ldualvsdi2  36295  omllaw3  36396  cmtcomlemN  36399  cmtbr3N  36405  omlfh3N  36410  llnexchb2lem  37019  dalawlem7  37028  dalawlem11  37032  dalawlem12  37033  pol1N  37061  paddatclN  37100  4atexlemcnd  37223  ltrncoidN  37279  cdleme3b  37380  cdleme11  37421  cdleme15a  37425  cdleme22e  37495  cdleme22g  37499  cdlemg18b  37830  trlcoat  37874  cdlemk2  37983  cdlemk4  37985  cdlemki  37992  cdlemksv2  37998  cdlemk15  38006  cdlemk55a  38110  diainN  38208  dia2dimlem3  38217  dia2dimlem5  38219  dvhlveclem  38259  diaocN  38276  cdlemn4  38349  cdlemn8  38355  dihopelvalcpre  38399  dihmeetlem9N  38466  dih1dimatlem  38480  dihpN  38487  dochvalr3  38514  dochsat  38534  djhjlj  38554  dochdmm1  38561  dihjatcclem4  38572  dihjat1  38580  dihjat4  38584  dochsnkr2cl  38625  dochfl1  38627  lclkrlem2j  38667  mapdordlem2  38788  mapdrvallem2  38796  hdmap10  38991  frlmvscadiccat  39194  frlmsnic  39198  negexpidd  39328  3cubeslem2  39331  3cubeslem3r  39333  mzpsubmpt  39389  irrapxlem3  39470  pellexlem6  39480  pell1234qrne0  39499  pell1234qrreccl  39500  pell1234qrmulcl  39501  pell14qrdich  39515  pell1qrgaplem  39519  rmxluc  39582  rmyluc  39583  jm2.24nn  39605  jm2.18  39634  jm2.19lem2  39636  jm2.19lem3  39637  jm2.22  39641  jm2.23  39642  jm2.16nn0  39650  jm2.27c  39653  fnwe2lem2  39700  lmhmfgsplit  39735  hbtlem2  39773  relexpmulnn  40103  relexpmulg  40104  ntrclsneine0lem  40463  int-addassocd  40576  dvconstbi  40715  bccm1k  40723  binomcxplemnotnn0  40737  fmptsnxp  41474  wessf1ornlem  41494  disjinfi  41503  projf1o  41508  infnsuprnmpt  41571  lefldiveq  41608  lt4addmuld  41622  fzdifsuc2  41626  suplesup  41656  infrpge  41668  xrlexaddrp  41669  xralrple2  41671  infleinflem1  41687  supminfrnmpt  41768  supminfxr2  41794  fsumnncl  41901  limcperiod  41958  sumnnodd  41960  limcresiooub  41972  limcresioolb  41973  0ellimcdiv  41979  reclimc  41983  limsupval3  42022  limsupequzmpt2  42048  liminfval5  42095  limsupresxr  42096  liminfresxr  42097  liminfvalxr  42113  liminfequzmpt2  42121  climliminflimsupd  42131  liminfltlem  42134  liminflbuz2  42145  sinmulcos  42195  coskpi2  42196  cncfdmsn  42222  cncfiooicclem1  42225  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  fperdvper  42252  dvmptresicc  42253  dvnmptdivc  42272  dvnxpaek  42276  dvnmul  42277  dvnprodlem1  42280  dvnprodlem3  42282  itgcoscmulx  42303  itgsincmulx  42308  itgspltprt  42313  itgiccshift  42314  itgperiod  42315  sublevolico  42318  volioof  42321  ovolsplit  42322  fvvolioof  42323  fvvolicof  42325  stoweidlem22  42356  stoweidlem32  42366  wallispilem5  42403  stirlinglem5  42412  dirkertrigeqlem2  42433  dirkertrigeq  42435  dirkercncflem1  42437  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem13  42454  fourierdlem16  42457  fourierdlem19  42460  fourierdlem21  42462  fourierdlem22  42463  fourierdlem28  42469  fourierdlem32  42473  fourierdlem33  42474  fourierdlem42  42483  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem56  42496  fourierdlem60  42500  fourierdlem61  42501  fourierdlem64  42504  fourierdlem66  42506  fourierdlem71  42511  fourierdlem73  42513  fourierdlem74  42514  fourierdlem76  42516  fourierdlem78  42518  fourierdlem79  42519  fourierdlem80  42520  fourierdlem81  42521  fourierdlem83  42523  fourierdlem88  42528  fourierdlem92  42532  fourierdlem93  42533  fourierdlem97  42537  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem109  42549  fourierdlem111  42551  fouriersw  42565  elaa2lem  42567  etransclem24  42592  etransclem25  42593  etransclem35  42603  etransclem46  42614  rrndistlt  42624  rrxunitopnfi  42626  qndenserrnbl  42629  qndenserrnopnlem  42631  saldifcl2  42660  intsal  42662  sge0sn  42710  sge0ltfirp  42731  sge0iunmptlemre  42746  sge0fodjrnlem  42747  sge0isum  42758  sge0xaddlem1  42764  nnfoctbdjlem  42786  meassle  42794  ismeannd  42798  meadif  42810  meaiuninclem  42811  meaiininclem  42817  omeunile  42836  caragendifcl  42845  caratheodory  42859  isomenndlem  42861  ovnsubaddlem1  42901  hoidmv1lelem2  42923  hoidmv1le  42925  hoidmvlelem2  42927  hoidmvle  42931  hoi2toco  42938  rrnmbl  42945  hoidifhspdmvle  42951  voncmpl  42952  hoiqssbl  42956  hspmbllem1  42957  hspmbllem2  42958  ovolval2lem  42974  ovolval5lem2  42984  ovnovollem1  42987  ovnovollem2  42988  hoimbl2  42996  vonhoire  43003  salpreimagelt  43035  salpreimalegt  43037  preimaioomnf  43046  smfres  43114  smfmullem1  43115  smflimmpt  43133  smfsupmpt  43138  smfinfmpt  43142  smflimsupmpt  43152  smfliminflem  43153  smfliminfmpt  43155  sigarcol  43170  f1oresf1o  43538  elsprel  43686  prproropf1o  43718  paireqne  43722  sfprmdvdsmersenne  43817  lighneallem3  43821  lighneallem4  43824  nn0onn0exALTV  43913  nnsum3primesprm  44004  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  c0snmgmhm  44234  rngcifuestrc  44317  funcrngcsetc  44318  funcrngcsetcALT  44319  funcringcsetc  44355  funcringcsetcALTV2lem7  44362  funcringcsetclem7ALTV  44385  lincext3  44560  lincresunit3  44585  nn0onn0ex  44632  nnpw2pmod  44692  blennn0em1  44700  digexp  44716  dignn0ehalf  44726  nn0mulfsum  44733  eenglngeehlnmlem2  44774  rrx2vlinest  44777  line2  44788  itschlc0xyqsol  44803  itsclinecirc0b  44810  recsec  44904  reccsc  44905  aacllem  44951  amgmlemALT  44953