Theorem eqtr2d 2797

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 2796	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2767	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 2733

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

This theorem is used by:  3eqtrrd  2801  3eqtr2rd  2803  ifan  4536  ifor  4537  dfopif  4830  fnco  6655  fnsnfv  6962  nvocnv  7287  elovmpt3rab1  7679  onsucmin  7830  csbopeq1a  8059  oaabs2  8651  ecinxp  8806  resixpfo  8957  sbthlem3  9101  rankxpsuc  9892  fseqenlem2  10097  dfac2b  10202  isf32lem9  10432  compsscnvlem  10441  ttukeylem7  10586  fpwwe2lem10  10718  00id  11478  submul2  11749  mulsubfacd  11770  divadddiv  12025  infrenegsup  12293  xadd4d  13426  fzdifsuc  13711  fzval3  13862  fzoshftral  13915  ceim1l  13980  fldiv  13993  flmod  14018  intfrac  14019  modcyc2  14040  modaddb  14042  moddi  14075  uzrdgfni  14094  axdc4uzlem  14119  seqf1olem1  14177  seqf1olem2  14178  seqid2  14184  expnegz  14232  binom2sub  14357  binom3  14361  hashreshashfun  14577  ccatw2s1p2  14778  ccats1pfxeq  14856  pfxccatin12lem2  14873  pfxccatin12  14875  swrdccat3b  14882  swrdrevpfx  14911  cshweqrep  14965  2cshwcshw  14969  ccatco  14979  swrds2  15084  relexpsucnnr  15171  relexpaddnn  15197  sgnmul  15253  reim  15269  mulre  15281  addcj  15308  absimle  15469  clim2ser  15815  isercoll2  15829  serf0  15841  iseralt  15845  summolem3  15873  isumclim3  15918  mptfzshft  15937  fsumrev  15938  fsum2mul  15948  incexc  15999  isumsplit  16002  mertenslem1  16046  fprodrev  16137  iprodclim3  16160  binomfallfaclem2  16199  ef4p  16274  tanval3  16295  efival  16313  sinmul  16333  bitsinvp1  16612  sadaddlem  16629  bitsshft  16638  smu01lem  16648  dfgcd2  16712  lcmgcdlem  16774  lcm1  16778  lcmfass  16814  eulerthlem2  16952  hashgcdeq  16960  powm2modprm  16974  pythagtriplem16  17001  pczpre  17018  pcqdiv  17028  pcadd  17060  pcfac  17070  prmreclem5  17091  4sqlem10  17118  4sqlem19  17134  vdwapun  17145  vdwlem1  17152  ramcl  17200  setsstruct  17347  strfvd  17371  strfv2d  17372  xpsff1o  17732  xpsrnbas  17736  2oppccomf  17892  oppcepi  17907  sscfn1  17985  sscfn2  17986  invfuc  18145  funcestrcsetclem7  18313  funcsetcestrclem7  18328  gsumsplit1r  18869  grpinvssd  19220  grpinvval2  19226  cycsubggend  19413  pmtrdifwrdellem2  19689  psgnunilem1  19700  psgnuni  19706  pgp0  19803  sylow1lem1  19805  sylow3lem2  19835  efgredleme  19950  efgcpbllemb  19962  frgpuptinv  19978  frgpup3lem  19984  gexexlem  20059  cyggenod  20091  gsumval3eu  20111  gsumval3  20114  gsumzaddlem  20128  dprd2db  20252  ablsimpgfindlem1  20316  ringinvdv  20637  c0snmgmhm  20685  rngcifuestrc  20884  funcrngcsetc  20885  funcrngcsetcALT  20886  funcringcsetc  20919  lss1d  21231  pwssplit1  21327  rhmqusnsg  21574  rngqiprnglin  21591  znzrh2  21844  regsumsupp  21921  ipassr2  21946  dsmmfi  22037  frlmlss  22050  frlmip  22077  frlmlbs  22096  frlmup3  22099  islindf4  22137  mplcoe3  22340  subrgascl  22368  evlseu  22385  psdadd  22477  ply1sclid  22600  ply1chr  22617  evls1addd  22682  evls1muld  22683  evls1vsca  22684  evls1maprhm  22687  evls1maplmhm  22688  evls1maprnss  22689  evl1maprhm  22690  1marepvmarrepid  22883  madurid  22952  smadiadetlem3  22976  matunitlindflem1  22987  matunitlindflem2  22988  mat2pmatghm  23041  pmatcollpwscmatlem1  23100  pm2mpmhmlem2  23130  cpmadurid  23178  cpmidgsumm2pm  23180  cpmadugsumlemB  23185  cayhamlem2  23195  ntrval2  23362  ordtuni  23501  cnclima  23579  cmpsub  23711  ptbasfi  23893  txbasval  23918  pt1hmeo  24118  alexsubALTlem1  24359  trust  24541  ussid  24572  ressuss  24574  ressprdsds  24683  imasdsf1olem  24685  setsms  24792  tmsxms  24798  tmsxpsmopn  24849  subgnm  24945  tngnm  24963  tngngp2  24964  xrsxmet  25122  xrge0gsumle  25146  metdstri  25164  xrhmeo  25260  lebnumlem3  25277  pcorevlem  25340  pi1xfrcnvlem  25370  clmabs  25397  cvsmuleqdivd  25448  rrxip  25704  rrxds  25707  rrxdsfi  25725  minveclem4a  25744  pjthlem1  25751  divcncf  25761  ovolunlem1a  25810  mbfres2  25959  i1faddlem  26007  ibladdlem  26133  iblabs  26142  ditgsplit  26174  dvmptresicc  26229  dvnres  26244  dvmptdiv  26287  dveflem  26292  dveq0  26313  dvfsumabs  26336  itgsubstlem  26361  ply1divex  26448  r1pid2  26473  dgrco  26587  plycjlem  26588  taylthlem1  26693  pserdv2  26750  abelthlem6  26756  abelthlem7  26758  tangtx  26827  abssinper  26842  sineq0  26845  explog  26915  reexplog  26916  eflogeq  26923  abslogle  26939  tanarg  26940  logtayl  26981  logtayl2  26983  relogbdiv  27100  ang180lem3  27132  affineequiv  27144  affineequiv2  27145  chordthmlem4  27156  chordthmlem5  27157  heron  27159  dcubic1lem  27164  dcubic2  27165  dcubic  27167  mcubic  27168  cubic2  27169  dquartlem1  27172  dquart  27174  quart1lem  27176  quartlem1  27178  quart  27182  acoscos  27214  atanlogaddlem  27234  atantayl2  27259  atantayl3  27260  birthdaylem2  27273  efrlim  27290  amgmlem  27310  logdifbnd  27314  emcllem3  27318  emcllem6  27321  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem4  27352  lgamgulmlem5  27353  gamigam  27373  lgamcvg2  27375  gamfac  27387  basellem3  27403  basellem8  27408  basellem9  27409  chtprm  27473  logfaclbnd  27542  perfect1  27548  bcp1ctr  27599  bclbnd  27600  bposlem1  27604  lgsdilem  27644  lgsdirnn0  27664  lgsdinn0  27665  gausslemma2dlem1a  27685  gausslemma2dlem4  27689  gausslemma2dlem5a  27690  lgseisenlem2  27696  lgsquadlem1  27700  2sqlem2  27738  mul2sq  27739  2sqmod  27756  2sqnn0  27758  vmadivsum  27802  rpvmasumlem  27807  dchrisumlem1  27809  dchrisumlem2  27810  dchrmusum2  27814  dchrvmasum2if  27817  dchrisum0lem2  27838  logsqvma2  27863  selberg3  27879  selberg4lem1  27880  pntrsumo1  27885  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem5  27901  pntibndlem2  27911  pntlemk  27926  pntlemo  27927  ostth2lem4  27956  ostth3  27958  flt4lem7  27982  subsfo  28444  negsval2  28445  ltonold  28640  noseqrdgfn  28685  n0fincut  28734  addhalfcut  28838  bdayfinbndlem1  28846  z12shalf  28859  tgbtwndiff  28962  tgifscgr  28964  trgcgrg  28971  motcgr3  29001  tgbtwnconn1lem1  29028  tgbtwnconn1lem2  29029  ismir  29124  miriso  29135  midexlem  29157  symquadprlnglem  29158  ragmir  29168  footexALT  29186  footexlem1  29187  footexlem2  29188  colperpexlem3  29201  mideulem2  29203  midex  29206  opphllem3  29218  midcgr  29278  lmiisolem  29294  prlngmid2  29432  quadcgrprlng  29437  brbtwn2  29476  colinearalglem4  29480  axsegconlem1  29488  axpaschlem  29511  axcontlem4  29538  axcontlem7  29541  axcontlem8  29542  ushgredgedgloop  29805  pfxwlk  30259  crctcshwlkn0lem6  30397  wwlknlsw  30429  wwlksnextwrd  30479  clwlkclwwlklem2a3  30578  clwlkclwwlk2  30587  clwwlkel  30630  clwwlkfo  30634  clwwlkext2edg  30640  eupth2eucrct  30811  numclwwlk2lem1lem  30936  numclwwlk1lem2fo  30952  numclwlk2lem2f  30971  grpoidinvlem2  31100  nvmtri  31266  cnnvm  31277  nvnd  31283  ipidsq  31305  ipnm  31306  ipipcj  31310  blocnilem  31399  ipasslem2  31427  dipsubdir  31443  hvaddsubval  31628  pjhthlem1  31986  pjspansn  32172  pjo  32266  unoplin  32515  adjadj  32531  hmoplin  32537  eigvec1  32557  lnopeqi  32603  nmcexi  32621  lnfnsubi  32641  riesz3i  32657  kbass6  32716  leoprf2  32722  leoprf  32723  pjnmopi  32743  mdslmd1lem1  32920  mdslmd1lem2  32921  superpos  32949  ifeq3da  33135  fgreu  33258  cocnvf1o  33314  resf1o  33315  quad3d  33334  fprodex01  33409  ccatws1f1o  33507  wrdt2ind  33509  mndlactfo  33581  mndractfo  33583  gsummpt2d  33603  gsummptp1  33611  xrge0tsmseq  33629  gsumwrd2dccatlem  33631  gsumwrd2dccat  33632  symgfcoeu  33636  wrdpmtrlast  33647  psgnfzto1stlem  33654  psgnfzto1st  33659  cycpm2tr  33673  cycpmco2lem6  33685  cycpmco2lem7  33686  subrgchr  33790  elrgspnlem1  33796  elrgspnlem3  33798  elrgspnsubrunlem1  33801  rloccring  33825  rhmdvd  33878  qusrn  33953  nsgqusf1olem3  33959  rhmquskerlem  33968  elrspunsn  33972  mxidlirredi  33989  qsdrngi  34012  1arithidomlem1  34060  1arithidomlem2  34061  evls1subd  34097  deg1prod  34108  0mplrim  34139  evlextv  34167  psrmonprod  34177  esplyfval1  34198  esplyind  34200  esplyindfv  34201  esplyfvn  34202  vietalem  34204  resssra  34212  dimval  34226  dimvalfi  34227  lindsunlem  34249  dimkerim  34252  qusdimsum  34253  fedgmullem1  34254  extdg1id  34291  fldextrspunlsplem  34298  fldextrspunlsp  34299  fldextrspunlem1  34300  fldextrspundgdvds  34306  extdgfialglem1  34317  extdgfialglem2  34318  ply1annidllem  34326  algextdeglem4  34345  constrrtcc  34360  constrsslem  34366  constrresqrtcl  34402  cos9thpiminplylem2  34408  cos9thpiminply  34413  madjusmdetlem2  34453  qtophaus  34461  zarclssn  34498  zarcmplem  34506  pstmval  34520  mndpluscn  34551  qqhucn  34617  esumval  34671  gsumesum  34684  esumcst  34688  esumpcvgval  34703  oddpwdc  34979  eulerpartlemgvv  35001  probdif  35045  signsvtn  35206  actfunsnf1o  35226  reprpmtf1o  35248  hgt750lemd  35270  logdivsqrle  35272  hgt750lemg  35276  hgt750lemb  35278  bnj1415  35661  vonf1oonfo  35877  derangen2  35918  subfaclefac  35920  subfaclim  35932  satom  36100  fmla  36125  mrsubrn  36257  sinccvglem  36416  bcprod  36482  nmulss1  36943  filnetlem4  37149  curunc  38505  ltflcei  38511  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem24  38542  mblfinlem4  38558  ibladdnclem  38574  iblabsnc  38582  iblmulc2nc  38583  ftc1anclem6  38596  ftc1anclem8  38598  sdclem2  38656  ismtycnv  38716  heiborlem10  38734  lflvsass  40118  lkrscss  40135  eqlkr  40136  eqlkr3  40138  ldualvsdi2  40181  omllaw3  40282  cmtcomlemN  40285  cmtbr3N  40291  omlfh3N  40296  llnexchb2lem  40905  dalawlem7  40914  dalawlem11  40918  dalawlem12  40919  pol1N  40947  paddatclN  40986  4atexlemcnd  41109  ltrncoidN  41165  cdleme3b  41266  cdleme11  41307  cdleme15a  41311  cdleme22e  41381  cdleme22g  41385  cdlemg18b  41716  trlcoat  41760  cdlemk2  41869  cdlemk4  41871  cdlemki  41878  cdlemksv2  41884  cdlemk15  41892  cdlemk55a  41996  diainN  42094  dia2dimlem3  42103  dia2dimlem5  42105  dvhlveclem  42145  diaocN  42162  cdlemn4  42235  cdlemn8  42241  dihopelvalcpre  42285  dihmeetlem9N  42352  dih1dimatlem  42366  dihpN  42373  dochvalr3  42400  dochsat  42420  djhjlj  42440  dochdmm1  42447  dihjatcclem4  42458  dihjat1  42466  dihjat4  42470  dochsnkr2cl  42511  dochfl1  42513  lclkrlem2j  42553  mapdordlem2  42674  mapdrvallem2  42682  hdmap10  42877  lcmineqlem12  43070  3lexlogpow5ineq5  43090  aks4d1p1  43106  primrootsunit1  43127  primrootscoprmpow  43129  posbezout  43130  aks6d1c1p3  43140  aks6d1c1p4  43141  aks6d1c1p5  43142  aks6d1c1p7  43143  evl1gprodd  43147  hashscontpow1  43151  aks6d1c3  43153  aks6d1c2lem3  43156  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c5lem3  43167  aks6d1c6lem1  43200  aks6d1c6isolem3  43206  aks6d1c6lem5  43207  bcle2d  43209  aks6d1c7lem1  43210  aks5lem3a  43219  grpods  43224  unitscyglem1  43225  unitscyglem2  43226  unitscyglem4  43228  unitscyglem5  43229  aks5lem7  43230  nicomachus  43349  sumcubes  43350  cnreeu  43534  frlmvscadiccat  43553  grpcominv1  43555  riccrng1  43562  ricdrng1  43572  frlmsnic  43584  evlselv  43597  fsuppind  43598  negexpidd  43672  3cubeslem2  43675  3cubeslem3r  43677  mzpsubmpt  43733  irrapxlem3  43810  pellexlem6  43820  pell1234qrne0  43839  pell1234qrreccl  43840  pell1234qrmulcl  43841  pell14qrdich  43855  pell1qrgaplem  43859  rmxluc  43922  rmyluc  43923  jm2.24nn  43945  jm2.18  43974  jm2.19lem2  43976  jm2.19lem3  43977  jm2.22  43981  jm2.23  43982  jm2.16nn0  43990  jm2.27c  43993  fnwe2lem2  44037  lmhmfgsplit  44072  hbtlem2  44110  onsucf1lem  44255  ofoafo  44342  naddcnffo  44350  naddwordnexlem4  44387  reabssgn  44621  relexpmulnn  44694  relexpmulg  44695  ntrclsneine0lem  45049  int-addassocd  45159  dvconstbi  45303  bccm1k  45311  binomcxplemnotnn0  45325  fmptsnxp  46153  wessf1ornlem  46169  projf1o  46180  infnsuprnmpt  46231  lefldiveq  46277  lt4addmuld  46291  fzdifsuc2  46295  suplesup  46320  infrpge  46332  xrlexaddrp  46333  xralrple2  46335  infleinflem1  46350  supminfrnmpt  46424  supminfxr2  46448  fsumnncl  46553  limcperiod  46609  sumnnodd  46611  limcresiooub  46621  limcresioolb  46622  0ellimcdiv  46628  reclimc  46632  limsupval3  46671  limsupequzmpt2  46697  liminfval5  46744  limsupresxr  46745  liminfresxr  46746  liminfvalxr  46762  liminfequzmpt2  46770  climliminflimsupd  46780  liminfltlem  46783  liminflbuz2  46794  sinmulcos  46844  coskpi2  46845  cncfdmsn  46869  cncfiooicclem1  46872  fprodsubrecnncnvlem  46886  fprodaddrecnncnvlem  46888  fperdvper  46898  dvnmptdivc  46917  dvnxpaek  46921  dvnmul  46922  dvnprodlem1  46925  dvnprodlem3  46927  itgcoscmulx  46948  itgsincmulx  46953  itgspltprt  46958  itgiccshift  46959  itgperiod  46960  sublevolico  46963  volioof  46966  ovolsplit  46967  fvvolioof  46968  fvvolicof  46970  stoweidlem22  47001  stoweidlem32  47011  wallispilem5  47048  stirlinglem5  47057  dirkertrigeqlem2  47078  dirkertrigeq  47080  dirkercncflem1  47082  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem13  47099  fourierdlem16  47102  fourierdlem19  47105  fourierdlem21  47107  fourierdlem22  47108  fourierdlem28  47114  fourierdlem32  47118  fourierdlem33  47119  fourierdlem42  47128  fourierdlem47  47132  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem56  47141  fourierdlem60  47145  fourierdlem61  47146  fourierdlem64  47149  fourierdlem66  47151  fourierdlem71  47156  fourierdlem73  47158  fourierdlem74  47159  fourierdlem76  47161  fourierdlem78  47163  fourierdlem79  47164  fourierdlem80  47165  fourierdlem81  47166  fourierdlem83  47168  fourierdlem88  47173  fourierdlem92  47177  fourierdlem93  47178  fourierdlem97  47182  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem109  47194  fourierdlem111  47196  fouriersw  47210  elaa2lem  47212  etransclem24  47237  etransclem25  47238  etransclem35  47248  etransclem46  47259  rrndistlt  47269  rrxunitopnfi  47271  qndenserrnbl  47274  qndenserrnopnlem  47276  saldifcl2  47307  intsal  47309  sge0sn  47358  sge0ltfirp  47379  sge0iunmptlemre  47394  sge0fodjrnlem  47395  sge0isum  47406  sge0xaddlem1  47412  nnfoctbdjlem  47434  meassle  47442  ismeannd  47446  meadif  47458  meaiuninclem  47459  meaiininclem  47465  omeunile  47484  caragendifcl  47493  caratheodory  47507  isomenndlem  47509  ovnsubaddlem1  47549  hoidmv1lelem2  47571  hoidmv1le  47573  hoidmvlelem2  47575  hoidmvle  47579  hoi2toco  47586  rrnmbl  47593  hoidifhspdmvle  47599  voncmpl  47600  hoiqssbl  47604  hspmbllem1  47605  hspmbllem2  47606  ovolval2lem  47622  ovolval5lem2  47632  ovnovollem1  47635  ovnovollem2  47636  hoimbl2  47644  vonhoire  47651  salpreimagelt  47686  salpreimalegt  47688  preimaioomnf  47698  smfres  47769  smfmullem1  47770  smflimmpt  47789  smfsupmpt  47794  smfinfmpt  47798  smflimsupmpt  47808  smfliminflem  47809  smfliminfmpt  47811  sigarcol  47843  sin5tlem2  47889  sinnpoly  47910  sqrtnpoly  47912  f1oresf1o  48329  elsprel  48526  prproropf1o  48558  paireqne  48562  sfprmdvdsmersenne  48657  lighneallem3  48661  lighneallem4  48664  nprmdvdsfacm1lem1  48674  nn0onn0exALTV  48766  nnsum3primesprm  48857  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  isuspgrim0lem  48960  clnbgrgrimlem  49000  uspgrlimlem3  49057  uspgrlimlem4  49058  gpgedgvtx0  49128  gpgedgvtx1  49129  funcringcsetcALTV2lem7  49362  funcringcsetclem7ALTV  49385  lincext3  49537  lincresunit3  49562  nn0onn0ex  49604  nnpw2pmod  49664  blennn0em1  49672  digexp  49688  dignn0ehalf  49698  nn0mulfsum  49705  itcovalpclem1  49751  eenglngeehlnmlem2  49819  rrx2vlinest  49822  line2  49833  itschlc0xyqsol  49848  itsclinecirc0b  49855  toplatjoin  50079  toplatmeet  50080  upeu2lem  50105  oppff1o  50226  imaf1co  50232  upciclem3  50245  natoppfb  50308  oppcthinco  50516  oppcthinendcALT  50518  lmddu  50744  recsec  50818  reccsc  50819  aacllem  50908  crossp3d  50936  amgmlemALT  50957