Theorem eqtr2d 2781

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 2780	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2746	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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  3eqtrrd  2785  3eqtr2rd  2787  ifan  4601  ifor  4602  dfopif  4894  fnco  6697  fnsnfv  7001  nvocnv  7317  elovmpt3rab1  7710  onsucmin  7857  csbopeq1a  8091  oaabs2  8705  ecinxp  8850  resixpfo  8994  sbthlem3  9151  rankxpsuc  9951  fseqenlem2  10094  dfac2b  10200  isf32lem9  10430  compsscnvlem  10439  ttukeylem7  10584  fpwwe2lem10  10709  00id  11465  submul2  11730  mulsubfacd  11751  divadddiv  12009  infrenegsup  12278  xadd4d  13365  fzdifsuc  13644  fzval3  13785  fzoshftral  13834  ceim1l  13898  fldiv  13911  flmod  13936  intfrac  13937  modcyc2  13958  moddi  13990  uzrdgfni  14009  axdc4uzlem  14034  seqf1olem1  14092  seqf1olem2  14093  seqid2  14099  expnegz  14147  binom2sub  14269  binom3  14273  hashreshashfun  14488  ccatw2s1p2  14685  ccats1pfxeq  14762  pfxccatin12lem2  14779  pfxccatin12  14781  swrdccat3b  14788  cshweqrep  14869  2cshwcshw  14874  ccatco  14884  swrds2  14989  relexpsucnnr  15074  relexpaddnn  15100  reim  15158  mulre  15170  addcj  15197  absimle  15358  clim2ser  15703  isercoll2  15717  serf0  15729  iseralt  15733  summolem3  15762  isumclim3  15807  mptfzshft  15826  fsumrev  15827  fsum2mul  15837  incexc  15885  isumsplit  15888  mertenslem1  15932  fprodrev  16025  iprodclim3  16048  binomfallfaclem2  16088  ef4p  16161  tanval3  16182  efival  16200  sinmul  16220  bitsinvp1  16495  sadaddlem  16512  bitsshft  16521  smu01lem  16531  dfgcd2  16593  lcmgcdlem  16653  lcm1  16657  lcmfass  16693  eulerthlem2  16829  hashgcdeq  16836  powm2modprm  16850  pythagtriplem16  16877  pczpre  16894  pcqdiv  16904  pcadd  16936  pcfac  16946  prmreclem5  16967  4sqlem10  16994  4sqlem19  17010  vdwapun  17021  vdwlem1  17028  ramcl  17076  setsstruct  17223  strfvd  17248  strfv2d  17249  xpsff1o  17627  xpsrnbas  17631  2oppccomf  17785  oppcepi  17800  sscfn1  17878  sscfn2  17879  invfuc  18044  funcestrcsetclem7  18215  funcsetcestrclem7  18230  gsumsplit1r  18725  grpinvssd  19057  grpinvval2  19063  cycsubggend  19245  pmtrdifwrdellem2  19524  psgnunilem1  19535  psgnuni  19541  pgp0  19638  sylow1lem1  19640  sylow3lem2  19670  efgredleme  19785  efgcpbllemb  19797  frgpuptinv  19813  frgpup3lem  19819  gexexlem  19894  cyggenod  19926  gsumval3eu  19946  gsumval3  19949  gsumzaddlem  19963  dprd2db  20087  ablsimpgfindlem1  20151  ringinvdv  20440  c0snmgmhm  20488  rngcifuestrc  20661  funcrngcsetc  20662  funcrngcsetcALT  20663  funcringcsetc  20696  lss1d  20984  pwssplit1  21081  rhmqusnsg  21318  rngqiprnglin  21335  znzrh2  21587  regsumsupp  21663  ipassr2  21688  dsmmfi  21781  frlmlss  21794  frlmip  21821  frlmlbs  21840  frlmup3  21843  islindf4  21881  mplcoe3  22079  subrgascl  22113  evlseu  22130  psdadd  22190  ply1sclid  22312  ply1chr  22331  evls1addd  22396  evls1muld  22397  evls1vsca  22398  evls1maprhm  22401  evls1maplmhm  22402  evls1maprnss  22403  evl1maprhm  22404  1marepvmarrepid  22602  madurid  22671  smadiadetlem3  22695  mat2pmatghm  22757  pmatcollpwscmatlem1  22816  pm2mpmhmlem2  22846  cpmadurid  22894  cpmidgsumm2pm  22896  cpmadugsumlemB  22901  cayhamlem2  22911  ntrval2  23080  ordtuni  23219  cnclima  23297  cmpsub  23429  ptbasfi  23610  txbasval  23635  pt1hmeo  23835  alexsubALTlem1  24076  trust  24259  ussid  24290  ressuss  24292  ressprdsds  24402  imasdsf1olem  24404  setsms  24513  tmsxms  24520  tmsxpsmopn  24571  subgnm  24667  tngnm  24693  tngngp2  24694  xrsxmet  24850  xrge0gsumle  24874  metdstri  24892  xrhmeo  24996  lebnumlem3  25014  pcorevlem  25078  pi1xfrcnvlem  25108  clmabs  25135  cvsmuleqdivd  25186  rrxip  25443  rrxds  25446  rrxdsfi  25464  minveclem4a  25483  pjthlem1  25490  divcncf  25501  ovolunlem1a  25550  mbfres2  25699  i1faddlem  25747  ibladdlem  25875  iblabs  25884  ditgsplit  25916  dvmptresicc  25971  dvnres  25987  dvmptdiv  26032  dveflem  26037  dveq0  26059  dvfsumabs  26083  itgsubstlem  26109  ply1divex  26196  r1pid2  26221  dgrco  26335  plycjlem  26336  taylthlem1  26433  pserdv2  26492  abelthlem6  26498  abelthlem7  26500  tangtx  26565  abssinper  26581  sineq0  26584  explog  26654  reexplog  26655  eflogeq  26662  abslogle  26678  tanarg  26679  logtayl  26720  logtayl2  26722  relogbdiv  26840  ang180lem3  26872  affineequiv  26884  affineequiv2  26885  chordthmlem4  26896  chordthmlem5  26897  heron  26899  dcubic1lem  26904  dcubic2  26905  dcubic  26907  mcubic  26908  cubic2  26909  dquartlem1  26912  dquart  26914  quart1lem  26916  quartlem1  26918  quart  26922  acoscos  26954  atanlogaddlem  26974  atantayl2  26999  atantayl3  27000  birthdaylem2  27013  efrlim  27030  efrlimOLD  27031  amgmlem  27051  logdifbnd  27055  emcllem3  27059  emcllem6  27062  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  gamigam  27114  lgamcvg2  27116  gamfac  27128  basellem3  27144  basellem8  27149  basellem9  27150  chtprm  27214  logfaclbnd  27284  perfect1  27290  bcp1ctr  27341  bclbnd  27342  bposlem1  27346  lgsdilem  27386  lgsdirnn0  27406  lgsdinn0  27407  gausslemma2dlem1a  27427  gausslemma2dlem4  27431  gausslemma2dlem5a  27432  lgseisenlem2  27438  lgsquadlem1  27442  2sqlem2  27480  mul2sq  27481  2sqmod  27498  2sqnn0  27500  vmadivsum  27544  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrmusum2  27556  dchrvmasum2if  27559  dchrisum0lem2  27580  logsqvma2  27605  selberg3  27621  selberg4lem1  27622  pntrsumo1  27627  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntibndlem2  27653  pntlemk  27668  pntlemo  27669  ostth2lem4  27698  ostth3  27700  subsfo  28113  negsval2  28114  sltonold  28301  noseqrdgfn  28330  addhalfcut  28437  tgbtwndiff  28532  tgifscgr  28534  trgcgrg  28541  motcgr3  28571  tgbtwnconn1lem1  28598  tgbtwnconn1lem2  28599  ismir  28685  miriso  28696  midexlem  28718  ragmir  28726  footexALT  28744  footexlem1  28745  footexlem2  28746  colperpexlem3  28758  mideulem2  28760  midex  28763  opphllem3  28775  midcgr  28806  lmiisolem  28822  brbtwn2  28938  colinearalglem4  28942  axsegconlem1  28950  axpaschlem  28973  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  ushgredgedgloop  29266  crctcshwlkn0lem6  29848  wwlknlsw  29880  wwlksnextwrd  29930  clwlkclwwlklem2a3  30026  clwlkclwwlk2  30035  clwwlkel  30078  clwwlkfo  30082  clwwlkext2edg  30088  eupth2eucrct  30249  numclwwlk2lem1lem  30374  numclwwlk1lem2fo  30390  numclwlk2lem2f  30409  grpoidinvlem2  30537  nvmtri  30703  cnnvm  30714  nvnd  30720  ipidsq  30742  ipnm  30743  ipipcj  30747  blocnilem  30836  ipasslem2  30864  dipsubdir  30880  hvaddsubval  31065  pjhthlem1  31423  pjspansn  31609  pjo  31703  unoplin  31952  adjadj  31968  hmoplin  31974  eigvec1  31994  lnopeqi  32040  nmcexi  32058  lnfnsubi  32078  riesz3i  32094  kbass6  32153  leoprf2  32159  leoprf  32160  pjnmopi  32180  mdslmd1lem1  32357  mdslmd1lem2  32358  superpos  32386  ifeq3da  32569  fgreu  32690  resf1o  32744  quad3d  32757  fprodex01  32829  ccatws1f1o  32918  wrdt2ind  32920  mndlactfo  33013  mndractfo  33015  gsummpt2d  33032  xrge0tsmseq  33043  symgfcoeu  33075  wrdpmtrlast  33086  psgnfzto1stlem  33093  psgnfzto1st  33098  cycpm2tr  33112  cycpmco2lem6  33124  cycpmco2lem7  33125  subrgchr  33217  rloccring  33242  rhmdvd  33313  qusrn  33402  nsgqusf1olem3  33408  rhmquskerlem  33418  elrspunsn  33422  mxidlirredi  33464  qsdrngi  33488  1arithidomlem1  33528  1arithidomlem2  33529  evls1subd  33562  r1pid2OLD  33594  resssra  33602  dimval  33613  dimvalfi  33614  lindsunlem  33637  dimkerim  33640  qusdimsum  33641  fedgmullem1  33642  extdg1id  33676  ply1annidllem  33694  algextdeglem4  33711  constrrtcc  33726  constrsslem  33731  madjusmdetlem2  33774  qtophaus  33782  zarclssn  33819  zarcmplem  33827  pstmval  33841  mndpluscn  33872  qqhucn  33938  esumval  34010  gsumesum  34023  esumcst  34027  esumpcvgval  34042  oddpwdc  34319  eulerpartlemgvv  34341  probdif  34385  sgnmul  34507  signsvtn  34561  actfunsnf1o  34581  reprpmtf1o  34603  hgt750lemd  34625  logdivsqrle  34627  hgt750lemg  34631  hgt750lemb  34633  bnj1415  35014  swrdrevpfx  35084  pfxwlk  35091  derangen2  35142  subfaclefac  35144  subfaclim  35156  satom  35324  fmla  35349  mrsubrn  35481  sinccvglem  35640  bcprod  35700  filnetlem4  36347  curunc  37562  ltflcei  37568  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  mblfinlem4  37620  ibladdnclem  37636  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem6  37658  ftc1anclem8  37660  sdclem2  37702  ismtycnv  37762  heiborlem10  37780  lflvsass  39037  lkrscss  39054  eqlkr  39055  eqlkr3  39057  ldualvsdi2  39100  omllaw3  39201  cmtcomlemN  39204  cmtbr3N  39210  omlfh3N  39215  llnexchb2lem  39825  dalawlem7  39834  dalawlem11  39838  dalawlem12  39839  pol1N  39867  paddatclN  39906  4atexlemcnd  40029  ltrncoidN  40085  cdleme3b  40186  cdleme11  40227  cdleme15a  40231  cdleme22e  40301  cdleme22g  40305  cdlemg18b  40636  trlcoat  40680  cdlemk2  40789  cdlemk4  40791  cdlemki  40798  cdlemksv2  40804  cdlemk15  40812  cdlemk55a  40916  diainN  41014  dia2dimlem3  41023  dia2dimlem5  41025  dvhlveclem  41065  diaocN  41082  cdlemn4  41155  cdlemn8  41161  dihopelvalcpre  41205  dihmeetlem9N  41272  dih1dimatlem  41286  dihpN  41293  dochvalr3  41320  dochsat  41340  djhjlj  41360  dochdmm1  41367  dihjatcclem4  41378  dihjat1  41386  dihjat4  41390  dochsnkr2cl  41431  dochfl1  41433  lclkrlem2j  41473  mapdordlem2  41594  mapdrvallem2  41602  hdmap10  41797  lcmineqlem12  41997  3lexlogpow5ineq5  42017  aks4d1p1  42033  primrootsunit1  42054  primrootscoprmpow  42056  posbezout  42057  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1p7  42070  evl1gprodd  42074  hashscontpow1  42078  aks6d1c3  42080  aks6d1c2lem3  42083  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5lem3  42094  aks6d1c6lem1  42127  aks6d1c6isolem3  42133  aks6d1c6lem5  42134  bcle2d  42136  aks6d1c7lem1  42137  aks5lem3a  42146  grpods  42151  unitscyglem1  42152  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  aks5lem7  42157  nicomachus  42300  sumcubes  42301  cnreeu  42446  frlmvscadiccat  42461  grpcominv1  42463  riccrng1  42476  ricdrng1  42483  frlmsnic  42495  evlselv  42542  fsuppind  42545  flt4lem7  42614  negexpidd  42638  3cubeslem2  42641  3cubeslem3r  42643  mzpsubmpt  42699  irrapxlem3  42780  pellexlem6  42790  pell1234qrne0  42809  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell14qrdich  42825  pell1qrgaplem  42829  rmxluc  42893  rmyluc  42894  jm2.24nn  42916  jm2.18  42945  jm2.19lem2  42947  jm2.19lem3  42948  jm2.22  42952  jm2.23  42953  jm2.16nn0  42961  jm2.27c  42964  fnwe2lem2  43008  lmhmfgsplit  43043  hbtlem2  43081  onsucf1lem  43231  ofoafo  43318  naddcnffo  43326  naddwordnexlem4  43363  reabssgn  43598  relexpmulnn  43671  relexpmulg  43672  ntrclsneine0lem  44026  int-addassocd  44136  dvconstbi  44303  bccm1k  44311  binomcxplemnotnn0  44325  fmptsnxp  45076  wessf1ornlem  45092  projf1o  45104  infnsuprnmpt  45159  lefldiveq  45207  lt4addmuld  45221  fzdifsuc2  45225  suplesup  45254  infrpge  45266  xrlexaddrp  45267  xralrple2  45269  infleinflem1  45285  supminfrnmpt  45360  supminfxr2  45384  fsumnncl  45493  limcperiod  45549  sumnnodd  45551  limcresiooub  45563  limcresioolb  45564  0ellimcdiv  45570  reclimc  45574  limsupval3  45613  limsupequzmpt2  45639  liminfval5  45686  limsupresxr  45687  liminfresxr  45688  liminfvalxr  45704  liminfequzmpt2  45712  climliminflimsupd  45722  liminfltlem  45725  liminflbuz2  45736  sinmulcos  45786  coskpi2  45787  cncfdmsn  45811  cncfiooicclem1  45814  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  fperdvper  45840  dvnmptdivc  45859  dvnxpaek  45863  dvnmul  45864  dvnprodlem1  45867  dvnprodlem3  45869  itgcoscmulx  45890  itgsincmulx  45895  itgspltprt  45900  itgiccshift  45901  itgperiod  45902  sublevolico  45905  volioof  45908  ovolsplit  45909  fvvolioof  45910  fvvolicof  45912  stoweidlem22  45943  stoweidlem32  45953  wallispilem5  45990  stirlinglem5  45999  dirkertrigeqlem2  46020  dirkertrigeq  46022  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem13  46041  fourierdlem16  46044  fourierdlem19  46047  fourierdlem21  46049  fourierdlem22  46050  fourierdlem28  46056  fourierdlem32  46060  fourierdlem33  46061  fourierdlem42  46070  fourierdlem47  46074  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem56  46083  fourierdlem60  46087  fourierdlem61  46088  fourierdlem64  46091  fourierdlem66  46093  fourierdlem71  46098  fourierdlem73  46100  fourierdlem74  46101  fourierdlem76  46103  fourierdlem78  46105  fourierdlem79  46106  fourierdlem80  46107  fourierdlem81  46108  fourierdlem83  46110  fourierdlem88  46115  fourierdlem92  46119  fourierdlem93  46120  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem109  46136  fourierdlem111  46138  fouriersw  46152  elaa2lem  46154  etransclem24  46179  etransclem25  46180  etransclem35  46190  etransclem46  46201  rrndistlt  46211  rrxunitopnfi  46213  qndenserrnbl  46216  qndenserrnopnlem  46218  saldifcl2  46249  intsal  46251  sge0sn  46300  sge0ltfirp  46321  sge0iunmptlemre  46336  sge0fodjrnlem  46337  sge0isum  46348  sge0xaddlem1  46354  nnfoctbdjlem  46376  meassle  46384  ismeannd  46388  meadif  46400  meaiuninclem  46401  meaiininclem  46407  omeunile  46426  caragendifcl  46435  caratheodory  46449  isomenndlem  46451  ovnsubaddlem1  46491  hoidmv1lelem2  46513  hoidmv1le  46515  hoidmvlelem2  46517  hoidmvle  46521  hoi2toco  46528  rrnmbl  46535  hoidifhspdmvle  46541  voncmpl  46542  hoiqssbl  46546  hspmbllem1  46547  hspmbllem2  46548  ovolval2lem  46564  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  hoimbl2  46586  vonhoire  46593  salpreimagelt  46628  salpreimalegt  46630  preimaioomnf  46640  smfres  46711  smfmullem1  46712  smflimmpt  46731  smfsupmpt  46736  smfinfmpt  46740  smflimsupmpt  46750  smfliminflem  46751  smfliminfmpt  46753  sigarcol  46785  f1oresf1o  47205  elsprel  47349  prproropf1o  47381  paireqne  47385  sfprmdvdsmersenne  47477  lighneallem3  47481  lighneallem4  47484  nn0onn0exALTV  47573  nnsum3primesprm  47664  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  isuspgrim0lem  47755  clnbgrgrimlem  47785  uspgrlimlem3  47814  uspgrlimlem4  47815  funcringcsetcALTV2lem7  48019  funcringcsetclem7ALTV  48042  lincext3  48185  lincresunit3  48210  nn0onn0ex  48257  nnpw2pmod  48317  blennn0em1  48325  digexp  48341  dignn0ehalf  48351  nn0mulfsum  48358  itcovalpclem1  48404  eenglngeehlnmlem2  48472  rrx2vlinest  48475  line2  48486  itschlc0xyqsol  48501  itsclinecirc0b  48508  toplatjoin  48674  toplatmeet  48675  recsec  48848  reccsc  48849  aacllem  48895  amgmlemALT  48897