Theorem eqtr2d 2834

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

Syntax hints:   → wi 4   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  3eqtrrd  2838  3eqtr2rd  2840  ifan  4476  ifor  4477  dfopif  4760  nvocnv  7016  elovmpt3rab1  7385  onsucmin  7516  csbopeq1a  7731  oaabs2  8255  ecinxp  8355  resixpfo  8483  sbthlem3  8613  rankxpsuc  9295  fseqenlem2  9436  dfac2b  9541  isf32lem9  9772  compsscnvlem  9781  ttukeylem7  9926  fpwwe2lem11  10051  00id  10804  submul2  11069  mulsubfacd  11090  divadddiv  11344  infrenegsup  11611  xadd4d  12684  fzdifsuc  12962  fzval3  13101  fzoshftral  13149  ceim1l  13210  fldiv  13223  flmod  13248  intfrac  13249  modcyc2  13270  moddi  13302  uzrdgfni  13321  axdc4uzlem  13346  seqf1olem1  13405  seqf1olem2  13406  seqid2  13412  expnegz  13459  binom2sub  13577  binom3  13581  hashreshashfun  13796  ccatw2s1p2  13988  ccats1pfxeq  14067  pfxccatin12lem2  14084  pfxccatin12  14086  swrdccat3b  14093  cshweqrep  14174  2cshwcshw  14178  ccatco  14188  swrds2  14293  relexpsucnnr  14376  relexpaddnn  14402  reim  14460  mulre  14472  addcj  14499  absimle  14661  clim2ser  15003  isercoll2  15017  serf0  15029  iseralt  15033  summolem3  15063  isumclim3  15106  mptfzshft  15125  fsumrev  15126  fsum2mul  15136  incexc  15184  isumsplit  15187  mertenslem1  15232  fprodrev  15323  iprodclim3  15346  binomfallfaclem2  15386  ef4p  15458  tanval3  15479  efival  15497  sinmul  15517  bitsinvp1  15788  sadaddlem  15805  bitsshft  15814  smu01lem  15824  dfgcd2  15884  lcmgcdlem  15940  lcm1  15944  lcmfass  15980  eulerthlem2  16109  hashgcdeq  16116  powm2modprm  16130  pythagtriplem16  16157  pczpre  16174  pcqdiv  16184  pcadd  16215  pcfac  16225  prmreclem5  16246  4sqlem10  16273  4sqlem19  16289  vdwapun  16300  vdwlem1  16307  ramcl  16355  setsstruct  16515  strfvd  16520  strfv2d  16521  xpsff1o  16832  xpsrnbas  16836  2oppccomf  16987  oppcepi  17001  sscfn1  17079  sscfn2  17080  invfuc  17236  funcestrcsetclem7  17388  funcsetcestrclem7  17403  gsumsplit1r  17889  grpinvssd  18168  grpinvval2  18174  cycsubggend  18340  pmtrdifwrdellem2  18602  psgnunilem1  18613  psgnuni  18619  pgp0  18713  sylow1lem1  18715  sylow3lem2  18745  efgredleme  18861  efgcpbllemb  18873  frgpuptinv  18889  frgpup3lem  18895  gexexlem  18965  cyggenod  18996  gsumval3eu  19017  gsumval3  19020  gsumzaddlem  19034  dprd2db  19158  ablsimpgfindlem1  19222  ringinvdv  19440  lss1d  19728  pwssplit1  19824  znzrh2  20237  regsumsupp  20311  ipassr2  20336  dsmmfi  20427  frlmlss  20440  frlmip  20467  frlmlbs  20486  frlmup3  20489  islindf4  20527  mplcoe3  20706  subrgascl  20737  evlseu  20755  ply1sclid  20917  1marepvmarrepid  21180  madurid  21249  smadiadetlem3  21273  mat2pmatghm  21335  pmatcollpwscmatlem1  21394  pm2mpmhmlem2  21424  cpmadurid  21472  cpmidgsumm2pm  21474  cpmadugsumlemB  21479  cayhamlem2  21489  ntrval2  21656  ordtuni  21795  cnclima  21873  cmpsub  22005  ptbasfi  22186  txbasval  22211  pt1hmeo  22411  alexsubALTlem1  22652  trust  22835  ussid  22866  ressuss  22869  ressprdsds  22978  imasdsf1olem  22980  setsms  23087  tmsxms  23093  tmsxpsmopn  23144  subgnm  23239  tngnm  23257  tngngp2  23258  xrsxmet  23414  xrge0gsumle  23438  metdstri  23456  xrhmeo  23551  lebnumlem3  23568  pcorevlem  23631  pi1xfrcnvlem  23661  clmabs  23688  cvsmuleqdivd  23739  rrxip  23994  rrxds  23997  rrxdsfi  24015  minveclem4a  24034  pjthlem1  24041  divcncf  24051  ovolunlem1a  24100  mbfres2  24249  i1faddlem  24297  ibladdlem  24423  iblabs  24432  ditgsplit  24464  dvmptresicc  24519  dvnres  24534  dvmptdiv  24577  dveflem  24582  dveq0  24603  dvfsumabs  24626  itgsubstlem  24651  ply1divex  24737  dgrco  24872  plycjlem  24873  taylthlem1  24968  pserdv2  25025  abelthlem6  25031  abelthlem7  25033  tangtx  25098  abssinper  25113  sineq0  25116  explog  25185  reexplog  25186  eflogeq  25193  abslogle  25209  tanarg  25210  logtayl  25251  logtayl2  25253  relogbdiv  25365  ang180lem3  25397  affineequiv  25409  affineequiv2  25410  chordthmlem4  25421  chordthmlem5  25422  heron  25424  dcubic1lem  25429  dcubic2  25430  dcubic  25432  mcubic  25433  cubic2  25434  dquartlem1  25437  dquart  25439  quart1lem  25441  quartlem1  25443  quart  25447  acoscos  25479  atanlogaddlem  25499  atantayl2  25524  atantayl3  25525  birthdaylem2  25538  efrlim  25555  amgmlem  25575  logdifbnd  25579  emcllem3  25583  emcllem6  25586  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem5  25618  gamigam  25638  lgamcvg2  25640  gamfac  25652  basellem3  25668  basellem8  25673  basellem9  25674  chtprm  25738  logfaclbnd  25806  perfect1  25812  bcp1ctr  25863  bclbnd  25864  bposlem1  25868  lgsdilem  25908  lgsdirnn0  25928  lgsdinn0  25929  gausslemma2dlem1a  25949  gausslemma2dlem4  25953  gausslemma2dlem5a  25954  lgseisenlem2  25960  lgsquadlem1  25964  2sqlem2  26002  mul2sq  26003  2sqmod  26020  2sqnn0  26022  vmadivsum  26066  rpvmasumlem  26071  dchrisumlem1  26073  dchrisumlem2  26074  dchrmusum2  26078  dchrvmasum2if  26081  dchrisum0lem2  26102  logsqvma2  26127  selberg3  26143  selberg4lem1  26144  pntrsumo1  26149  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem5  26165  pntibndlem2  26175  pntlemk  26190  pntlemo  26191  ostth2lem4  26220  ostth3  26222  tgbtwndiff  26300  tgifscgr  26302  trgcgrg  26309  motcgr3  26339  tgbtwnconn1lem1  26366  tgbtwnconn1lem2  26367  ismir  26453  miriso  26464  midexlem  26486  ragmir  26494  footexALT  26512  footexlem1  26513  footexlem2  26514  colperpexlem3  26526  mideulem2  26528  midex  26531  opphllem3  26543  midcgr  26574  lmiisolem  26590  brbtwn2  26699  colinearalglem4  26703  axsegconlem1  26711  axpaschlem  26734  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  ushgredgedgloop  27021  crctcshwlkn0lem6  27601  wwlknlsw  27633  wwlksnextwrd  27683  clwlkclwwlklem2a3  27779  clwlkclwwlk2  27788  clwwlkel  27831  clwwlkfo  27835  clwwlkext2edg  27841  eupth2eucrct  28002  numclwwlk2lem1lem  28127  numclwwlk1lem2fo  28143  numclwlk2lem2f  28162  grpoidinvlem2  28288  nvmtri  28454  cnnvm  28465  nvnd  28471  ipidsq  28493  ipnm  28494  ipipcj  28498  blocnilem  28587  ipasslem2  28615  dipsubdir  28631  hvaddsubval  28816  pjhthlem1  29174  pjspansn  29360  pjo  29454  unoplin  29703  adjadj  29719  hmoplin  29725  eigvec1  29745  lnopeqi  29791  nmcexi  29809  lnfnsubi  29829  riesz3i  29845  kbass6  29904  leoprf2  29910  leoprf  29911  pjnmopi  29931  mdslmd1lem1  30108  mdslmd1lem2  30109  superpos  30137  ifeq3da  30313  fgreu  30435  resf1o  30492  fprodex01  30567  wrdt2ind  30653  gsummpt2d  30734  xrge0tsmseq  30744  symgfcoeu  30776  psgnfzto1stlem  30792  psgnfzto1st  30797  cycpm2tr  30811  cycpmco2lem6  30823  cycpmco2lem7  30824  subrgchr  30916  rhmdvd  30945  dimval  31089  dimvalfi  31090  lindsunlem  31108  dimkerim  31111  qusdimsum  31112  fedgmullem1  31113  extdg1id  31141  madjusmdetlem2  31181  qtophaus  31189  zarclssn  31226  zarcmplem  31234  pstmval  31248  mndpluscn  31279  qqhucn  31343  esumval  31415  gsumesum  31428  esumcst  31432  esumpcvgval  31447  oddpwdc  31722  eulerpartlemgvv  31744  probdif  31788  sgnmul  31910  signsvtn  31964  actfunsnf1o  31985  reprpmtf1o  32007  hgt750lemd  32029  logdivsqrle  32031  hgt750lemg  32035  hgt750lemb  32037  bnj1415  32420  swrdrevpfx  32476  pfxwlk  32483  derangen2  32534  subfaclefac  32536  subfaclim  32548  satom  32716  fmla  32741  mrsubrn  32873  sinccvglem  33028  bcprod  33083  filnetlem4  33842  curunc  35039  ltflcei  35045  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem24  35081  mblfinlem4  35097  ibladdnclem  35113  iblabsnc  35121  iblmulc2nc  35122  ftc1anclem6  35135  ftc1anclem8  35137  sdclem2  35180  ismtycnv  35240  heiborlem10  35258  lflvsass  36377  lkrscss  36394  eqlkr  36395  eqlkr3  36397  ldualvsdi2  36440  omllaw3  36541  cmtcomlemN  36544  cmtbr3N  36550  omlfh3N  36555  llnexchb2lem  37164  dalawlem7  37173  dalawlem11  37177  dalawlem12  37178  pol1N  37206  paddatclN  37245  4atexlemcnd  37368  ltrncoidN  37424  cdleme3b  37525  cdleme11  37566  cdleme15a  37570  cdleme22e  37640  cdleme22g  37644  cdlemg18b  37975  trlcoat  38019  cdlemk2  38128  cdlemk4  38130  cdlemki  38137  cdlemksv2  38143  cdlemk15  38151  cdlemk55a  38255  diainN  38353  dia2dimlem3  38362  dia2dimlem5  38364  dvhlveclem  38404  diaocN  38421  cdlemn4  38494  cdlemn8  38500  dihopelvalcpre  38544  dihmeetlem9N  38611  dih1dimatlem  38625  dihpN  38632  dochvalr3  38659  dochsat  38679  djhjlj  38699  dochdmm1  38706  dihjatcclem4  38717  dihjat1  38725  dihjat4  38729  dochsnkr2cl  38770  dochfl1  38772  lclkrlem2j  38812  mapdordlem2  38933  mapdrvallem2  38941  hdmap10  39136  lcmineqlem12  39328  frlmvscadiccat  39440  frlmsnic  39453  fsuppind  39456  cnreeu  39593  negexpidd  39623  3cubeslem2  39626  3cubeslem3r  39628  mzpsubmpt  39684  irrapxlem3  39765  pellexlem6  39775  pell1234qrne0  39794  pell1234qrreccl  39795  pell1234qrmulcl  39796  pell14qrdich  39810  pell1qrgaplem  39814  rmxluc  39877  rmyluc  39878  jm2.24nn  39900  jm2.18  39929  jm2.19lem2  39931  jm2.19lem3  39932  jm2.22  39936  jm2.23  39937  jm2.16nn0  39945  jm2.27c  39948  fnwe2lem2  39995  lmhmfgsplit  40030  hbtlem2  40068  reabssgn  40336  relexpmulnn  40410  relexpmulg  40411  ntrclsneine0lem  40767  int-addassocd  40880  dvconstbi  41038  bccm1k  41046  binomcxplemnotnn0  41060  fmptsnxp  41793  wessf1ornlem  41811  projf1o  41825  infnsuprnmpt  41888  lefldiveq  41924  lt4addmuld  41938  fzdifsuc2  41942  suplesup  41971  infrpge  41983  xrlexaddrp  41984  xralrple2  41986  infleinflem1  42002  supminfrnmpt  42082  supminfxr2  42108  fsumnncl  42213  limcperiod  42270  sumnnodd  42272  limcresiooub  42284  limcresioolb  42285  0ellimcdiv  42291  reclimc  42295  limsupval3  42334  limsupequzmpt2  42360  liminfval5  42407  limsupresxr  42408  liminfresxr  42409  liminfvalxr  42425  liminfequzmpt2  42433  climliminflimsupd  42443  liminfltlem  42446  liminflbuz2  42457  sinmulcos  42507  coskpi2  42508  cncfdmsn  42532  cncfiooicclem1  42535  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  fperdvper  42561  dvnmptdivc  42580  dvnxpaek  42584  dvnmul  42585  dvnprodlem1  42588  dvnprodlem3  42590  itgcoscmulx  42611  itgsincmulx  42616  itgspltprt  42621  itgiccshift  42622  itgperiod  42623  sublevolico  42626  volioof  42629  ovolsplit  42630  fvvolioof  42631  fvvolicof  42633  stoweidlem22  42664  stoweidlem32  42674  wallispilem5  42711  stirlinglem5  42720  dirkertrigeqlem2  42741  dirkertrigeq  42743  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem13  42762  fourierdlem16  42765  fourierdlem19  42768  fourierdlem21  42770  fourierdlem22  42771  fourierdlem28  42777  fourierdlem32  42781  fourierdlem33  42782  fourierdlem42  42791  fourierdlem47  42795  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem56  42804  fourierdlem60  42808  fourierdlem61  42809  fourierdlem64  42812  fourierdlem66  42814  fourierdlem71  42819  fourierdlem73  42821  fourierdlem74  42822  fourierdlem76  42824  fourierdlem78  42826  fourierdlem79  42827  fourierdlem80  42828  fourierdlem81  42829  fourierdlem83  42831  fourierdlem88  42836  fourierdlem92  42840  fourierdlem93  42841  fourierdlem97  42845  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem109  42857  fourierdlem111  42859  fouriersw  42873  elaa2lem  42875  etransclem24  42900  etransclem25  42901  etransclem35  42911  etransclem46  42922  rrndistlt  42932  rrxunitopnfi  42934  qndenserrnbl  42937  qndenserrnopnlem  42939  saldifcl2  42968  intsal  42970  sge0sn  43018  sge0ltfirp  43039  sge0iunmptlemre  43054  sge0fodjrnlem  43055  sge0isum  43066  sge0xaddlem1  43072  nnfoctbdjlem  43094  meassle  43102  ismeannd  43106  meadif  43118  meaiuninclem  43119  meaiininclem  43125  omeunile  43144  caragendifcl  43153  caratheodory  43167  isomenndlem  43169  ovnsubaddlem1  43209  hoidmv1lelem2  43231  hoidmv1le  43233  hoidmvlelem2  43235  hoidmvle  43239  hoi2toco  43246  rrnmbl  43253  hoidifhspdmvle  43259  voncmpl  43260  hoiqssbl  43264  hspmbllem1  43265  hspmbllem2  43266  ovolval2lem  43282  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296  hoimbl2  43304  vonhoire  43311  salpreimagelt  43343  salpreimalegt  43345  preimaioomnf  43354  smfres  43422  smfmullem1  43423  smflimmpt  43441  smfsupmpt  43446  smfinfmpt  43450  smflimsupmpt  43460  smfliminflem  43461  smfliminfmpt  43463  sigarcol  43478  f1oresf1o  43846  elsprel  43992  prproropf1o  44024  paireqne  44028  sfprmdvdsmersenne  44121  lighneallem3  44125  lighneallem4  44128  nn0onn0exALTV  44217  nnsum3primesprm  44308  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  c0snmgmhm  44538  rngcifuestrc  44621  funcrngcsetc  44622  funcrngcsetcALT  44623  funcringcsetc  44659  funcringcsetcALTV2lem7  44666  funcringcsetclem7ALTV  44689  lincext3  44865  lincresunit3  44890  nn0onn0ex  44937  nnpw2pmod  44997  blennn0em1  45005  digexp  45021  dignn0ehalf  45031  nn0mulfsum  45038  itcovalpclem1  45084  eenglngeehlnmlem2  45152  rrx2vlinest  45155  line2  45166  itschlc0xyqsol  45181  itsclinecirc0b  45188  recsec  45282  reccsc  45283  aacllem  45329  amgmlemALT  45331