Theorem eqtr2d 2862

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

Syntax hints:   → wi 4   = wceq 1656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818

This theorem is referenced by:  3eqtrrd  2866  3eqtr2rd  2868  ifan  4357  ifor  4358  dfopif  4620  nvocnv  6792  elovmpt3rab1  7153  onsucmin  7282  csbopeq1a  7483  oaabs2  7992  ecinxp  8087  resixpfo  8213  sbthlem3  8341  rankxpsuc  9022  fseqenlem2  9161  dfac2b  9266  dfac2OLD  9268  isf32lem9  9498  compsscnvlem  9507  ttukeylem7  9652  fpwwe2lem11  9777  00id  10530  submul2  10794  mulsubfacd  10816  divadddiv  11066  infrenegsup  11336  xadd4d  12421  fzdifsuc  12694  fzval3  12832  fzoshftral  12880  ceim1l  12941  fldiv  12954  flmod  12979  intfrac  12980  modcyc2  13001  moddi  13033  uzrdgfni  13052  axdc4uzlem  13077  seqf1olem1  13134  seqf1olem2  13135  seqid2  13141  expnegz  13188  binom2sub  13275  binom3  13279  hashreshashfun  13515  ccatw2s1p2  13697  ccats1pfxeq  13801  ccats1swrdeqOLD  13802  pfxccatin12lem2  13828  swrdccatin12lem2OLD  13829  pfxccatin12  13831  swrdccatin12OLD  13832  swrdccat3b  13842  swrdccat3bOLD  13843  cshweqrep  13942  2cshwcshw  13946  ccatco  13956  swrds2  14061  relexpsucnnr  14142  relexpaddnn  14168  reim  14226  mulre  14238  addcj  14265  absimle  14426  clim2ser  14762  isercoll2  14776  serf0  14788  iseralt  14792  summolem3  14822  isumclim3  14865  mptfzshft  14884  fsumrev  14885  fsum2mul  14895  incexc  14943  isumsplit  14946  mertenslem1  14989  fprodrev  15080  iprodclim3  15103  binomfallfaclem2  15143  ef4p  15215  tanval3  15236  efival  15254  sinmul  15274  bitsinvp1  15544  sadaddlem  15561  bitsshft  15570  smu01lem  15580  dfgcd2  15636  lcmgcdlem  15692  lcm1  15696  lcmfass  15732  eulerthlem2  15858  hashgcdeq  15865  powm2modprm  15879  pythagtriplem16  15906  pczpre  15923  pcqdiv  15933  pcadd  15964  pcfac  15974  prmreclem5  15995  4sqlem10  16022  4sqlem19  16038  vdwapun  16049  vdwlem1  16056  ramcl  16104  setsstruct  16262  strfvd  16267  strfv2d  16268  xpsff1o  16581  xpslem  16586  2oppccomf  16737  oppcepi  16751  sscfn1  16829  sscfn2  16830  invfuc  16986  funcestrcsetclem7  17139  funcsetcestrclem7  17154  grpinvssd  17846  grpinvval2  17852  pmtrdifwrdellem2  18252  psgnunilem1  18263  psgnuni  18270  pgp0  18362  sylow1lem1  18364  sylow3lem2  18394  efgredleme  18508  efgcpbllemb  18521  frgpuptinv  18537  frgpup3lem  18543  gexexlem  18608  cyggenod  18639  gsumval3eu  18658  gsumval3  18661  gsumzaddlem  18674  dprd2db  18796  ringinvdv  19048  lss1d  19322  pwssplit1  19418  mplcoe3  19827  subrgascl  19858  evlseu  19876  ply1sclid  20018  znzrh2  20253  regsumsupp  20329  ipassr2  20354  dsmmfi  20445  frlmlss  20458  frlmip  20484  frlmlbs  20503  frlmup3  20506  islindf4  20544  1marepvmarrepid  20749  madurid  20818  smadiadetlem3  20843  mat2pmatghm  20905  pmatcollpwscmatlem1  20964  pm2mpmhmlem2  20994  cpmadurid  21042  cpmidgsumm2pm  21044  cpmadugsumlemB  21049  cayhamlem2  21059  ntrval2  21226  ordtuni  21365  cnclima  21443  cmpsub  21574  ptbasfi  21755  txbasval  21780  pt1hmeo  21980  alexsubALTlem1  22221  trust  22403  ussid  22434  ressuss  22437  ressprdsds  22546  imasdsf1olem  22548  setsms  22655  tmsxms  22661  tmsxpsmopn  22712  subgnm  22807  tngnm  22825  tngngp2  22826  xrsxmet  22982  xrge0gsumle  23006  metdstri  23024  xrhmeo  23115  lebnumlem3  23132  pcorevlem  23195  pi1xfrcnvlem  23225  clmabs  23252  cvsmuleqdivd  23303  rrxip  23558  rrxds  23561  rrxdsfi  23579  minveclem4a  23598  pjthlem1  23605  divcncf  23613  ovolunlem1a  23662  mbfres2  23811  i1faddlem  23859  ibladdlem  23985  iblabs  23994  ditgsplit  24024  dvnres  24093  dvmptdiv  24136  dveflem  24141  dveq0  24162  dvfsumabs  24185  itgsubstlem  24210  ply1divex  24295  dgrco  24430  plycjlem  24431  taylthlem1  24526  pserdv2  24583  abelthlem6  24589  abelthlem7  24591  tangtx  24657  abssinper  24670  sineq0  24673  explog  24739  reexplog  24740  eflogeq  24747  abslogle  24763  tanarg  24764  logtayl  24805  logtayl2  24807  relogbdiv  24919  ang180lem3  24951  affineequiv  24963  affineequiv2  24964  chordthmlem4  24975  chordthmlem5  24976  heron  24978  dcubic1lem  24983  dcubic2  24984  dcubic  24986  mcubic  24987  cubic2  24988  dquartlem1  24991  dquart  24993  quart1lem  24995  quartlem1  24997  quart  25001  acoscos  25033  atanlogaddlem  25053  atantayl2  25078  atantayl3  25079  birthdaylem2  25092  efrlim  25109  amgmlem  25129  logdifbnd  25133  emcllem3  25137  emcllem6  25140  lgamgulmlem2  25169  lgamgulmlem3  25170  lgamgulmlem4  25171  lgamgulmlem5  25172  gamigam  25192  lgamcvg2  25194  gamfac  25206  basellem3  25222  basellem8  25227  basellem9  25228  chtprm  25292  logfaclbnd  25360  perfect1  25366  bcp1ctr  25417  bclbnd  25418  bposlem1  25422  lgsdilem  25462  lgsdirnn0  25482  lgsdinn0  25483  gausslemma2dlem1a  25503  gausslemma2dlem4  25507  gausslemma2dlem5a  25508  lgseisenlem2  25514  lgsquadlem1  25518  2sqlem2  25556  mul2sq  25557  vmadivsum  25584  rpvmasumlem  25589  dchrisumlem1  25591  dchrisumlem2  25592  dchrmusum2  25596  dchrvmasum2if  25599  dchrisum0lem2  25620  logsqvma2  25645  selberg3  25661  selberg4lem1  25662  pntrsumo1  25667  pntrlog2bndlem2  25680  pntrlog2bndlem3  25681  pntrlog2bndlem5  25683  pntibndlem2  25693  pntlemk  25708  pntlemo  25709  ostth2lem4  25738  ostth3  25740  tgbtwndiff  25818  tgifscgr  25820  trgcgrg  25827  motcgr3  25857  tgbtwnconn1lem1  25884  tgbtwnconn1lem2  25885  ismir  25971  miriso  25982  midexlem  26004  ragmir  26012  footex  26030  colperpexlem3  26041  mideulem2  26043  midex  26046  opphllem3  26058  midcgr  26089  lmiisolem  26105  brbtwn2  26204  colinearalglem4  26208  axsegconlem1  26216  axpaschlem  26239  axcontlem4  26266  axcontlem7  26269  axcontlem8  26270  ushgredgedgloop  26527  ushgredgedgloopOLD  26528  crctcshwlkn0lem6  27114  wwlknlsw  27146  wwlksnextwrd  27211  wwlksnextwrdOLD  27216  clwwlkccatlem  27318  clwlkclwwlklem2a3  27323  clwlkclwwlk2  27333  clwlkclwwlk2OLD  27334  clwwlkel  27385  clwwlkfoOLD  27389  clwwlkfo  27394  clwwlkext2edg  27401  wwlksext2clwwlk  27402  eupth2eucrct  27583  numclwwlk2lem1lem  27712  numclwwlk1lem2fo  27738  numclwwlk1lem2foOLD  27743  numclwlk2lem2f  27769  numclwlk2lem2fOLD  27772  numclwlk2lem2fOLDOLD  27780  grpoidinvlem2  27904  nvmtri  28070  cnnvm  28081  nvnd  28087  ipidsq  28109  ipnm  28110  ipipcj  28114  blocnilem  28203  ipasslem2  28231  dipsubdir  28247  hvaddsubval  28434  pjhthlem1  28794  pjspansn  28980  pjo  29074  unoplin  29323  adjadj  29339  hmoplin  29345  eigvec1  29365  lnopeqi  29411  nmcexi  29429  lnfnsubi  29449  riesz3i  29465  kbass6  29524  leoprf2  29530  leoprf  29531  pjnmopi  29551  mdslmd1lem1  29728  mdslmd1lem2  29729  superpos  29757  ifeq3da  29902  fgreu  30008  resf1o  30042  fprodex01  30107  2sqmod  30182  gsummpt2d  30315  xrge0tsmseq  30321  subrgchr  30328  rhmdvd  30355  symgfcoeu  30379  psgnfzto1stlem  30384  psgnfzto1st  30389  madjusmdetlem2  30428  qtophaus  30437  pstmval  30472  mndpluscn  30506  qqhucn  30570  esumval  30642  gsumesum  30655  esumcst  30659  esumpcvgval  30674  oddpwdc  30950  eulerpartlemgvv  30972  probdif  31017  sgnmul  31139  signsvtn  31199  actfunsnf1o  31220  reprpmtf1o  31242  hgt750lemd  31264  logdivsqrle  31266  hgt750lemg  31270  hgt750lemb  31272  bnj1415  31641  derangen2  31691  subfaclefac  31693  subfaclim  31705  mrsubrn  31945  sinccvglem  32099  bcprod  32155  filnetlem4  32903  curunc  33927  ltflcei  33933  matunitlindflem1  33942  matunitlindflem2  33943  poimirlem16  33962  poimirlem17  33963  poimirlem19  33965  poimirlem20  33966  poimirlem24  33970  mblfinlem4  33986  ibladdnclem  34002  iblabsnc  34010  iblmulc2nc  34011  ftc1anclem6  34026  ftc1anclem8  34028  sdclem2  34073  ismtycnv  34136  heiborlem10  34154  lflvsass  35149  lkrscss  35166  eqlkr  35167  eqlkr3  35169  ldualvsdi2  35212  omllaw3  35313  cmtcomlemN  35316  cmtbr3N  35322  omlfh3N  35327  llnexchb2lem  35936  dalawlem7  35945  dalawlem11  35949  dalawlem12  35950  pol1N  35978  paddatclN  36017  4atexlemcnd  36140  ltrncoidN  36196  cdleme3b  36297  cdleme11  36338  cdleme15a  36342  cdleme22e  36412  cdleme22g  36416  cdlemg18b  36747  trlcoat  36791  cdlemk2  36900  cdlemk4  36902  cdlemki  36909  cdlemksv2  36915  cdlemk15  36923  cdlemk55a  37027  diainN  37125  dia2dimlem3  37134  dia2dimlem5  37136  dvhlveclem  37176  diaocN  37193  cdlemn4  37266  cdlemn8  37272  dihopelvalcpre  37316  dihmeetlem9N  37383  dih1dimatlem  37397  dihpN  37404  dochvalr3  37431  dochsat  37451  djhjlj  37471  dochdmm1  37478  dihjatcclem4  37489  dihjat1  37497  dihjat4  37501  dochsnkr2cl  37542  dochfl1  37544  lclkrlem2j  37584  mapdordlem2  37705  mapdrvallem2  37713  hdmap10  37908  mzpsubmpt  38143  irrapxlem3  38225  pellexlem6  38235  pell1234qrne0  38254  pell1234qrreccl  38255  pell1234qrmulcl  38256  pell14qrdich  38270  pell1qrgaplem  38274  rmxluc  38337  rmyluc  38338  jm2.24nn  38362  jm2.18  38391  jm2.19lem2  38393  jm2.19lem3  38394  jm2.22  38398  jm2.23  38399  jm2.16nn0  38407  jm2.27c  38410  fnwe2lem2  38457  lmhmfgsplit  38492  hbtlem2  38530  relexpmulnn  38835  relexpmulg  38836  ntrclsneine0lem  39195  int-addassocd  39310  dvconstbi  39366  bccm1k  39374  binomcxplemnotnn0  39388  fmptsnxp  40151  wessf1ornlem  40172  founiiun0  40178  disjinfi  40181  projf1o  40187  infnsuprnmpt  40258  lefldiveq  40297  lt4addmuld  40311  fzdifsuc2  40315  suplesup  40345  infrpge  40357  xrlexaddrp  40358  xralrple2  40360  infleinflem1  40376  supminfrnmpt  40460  supminfxr2  40486  fsumnncl  40591  limcperiod  40648  sumnnodd  40650  limcresiooub  40662  limcresioolb  40663  0ellimcdiv  40669  reclimc  40673  limsupval3  40712  limsupequzmpt2  40738  liminfval5  40785  limsupresxr  40786  liminfresxr  40787  liminfvalxr  40803  liminfequzmpt2  40811  climliminflimsupd  40821  liminfltlem  40824  sinmulcos  40864  coskpi2  40865  cncfdmsn  40891  cncfiooicclem1  40894  fprodsubrecnncnvlem  40909  fprodaddrecnncnvlem  40911  fperdvper  40921  dvmptresicc  40922  dvnmptdivc  40941  dvnxpaek  40945  dvnmul  40946  dvnprodlem1  40949  dvnprodlem3  40951  itgcoscmulx  40972  itgsincmulx  40977  itgspltprt  40982  itgiccshift  40983  itgperiod  40984  sublevolico  40988  volioof  40991  ovolsplit  40992  fvvolioof  40993  fvvolicof  40995  stoweidlem22  41026  stoweidlem32  41036  wallispilem5  41073  stirlinglem5  41082  dirkertrigeqlem2  41103  dirkertrigeq  41105  dirkercncflem1  41107  dirkercncflem2  41108  dirkercncflem4  41110  fourierdlem13  41124  fourierdlem16  41127  fourierdlem19  41130  fourierdlem21  41132  fourierdlem22  41133  fourierdlem28  41139  fourierdlem32  41143  fourierdlem33  41144  fourierdlem42  41153  fourierdlem47  41157  fourierdlem48  41158  fourierdlem49  41159  fourierdlem50  41160  fourierdlem56  41166  fourierdlem60  41170  fourierdlem61  41171  fourierdlem64  41174  fourierdlem66  41176  fourierdlem71  41181  fourierdlem73  41183  fourierdlem74  41184  fourierdlem76  41186  fourierdlem78  41188  fourierdlem79  41189  fourierdlem80  41190  fourierdlem81  41191  fourierdlem83  41193  fourierdlem88  41198  fourierdlem92  41202  fourierdlem93  41203  fourierdlem97  41207  fourierdlem101  41211  fourierdlem103  41213  fourierdlem104  41214  fourierdlem109  41219  fourierdlem111  41221  fouriersw  41235  elaa2lem  41237  etransclem24  41262  etransclem25  41263  etransclem35  41273  etransclem46  41284  rrndistlt  41294  rrxunitopnfi  41296  qndenserrnbl  41299  qndenserrnopnlem  41301  saldifcl2  41330  intsal  41332  sge0sn  41380  sge0ltfirp  41401  sge0iunmptlemre  41416  sge0fodjrnlem  41417  sge0isum  41428  sge0xaddlem1  41434  nnfoctbdjlem  41456  meassle  41464  ismeannd  41468  meadif  41480  meaiuninclem  41481  meaiininclem  41487  omeunile  41506  caragendifcl  41515  caratheodory  41529  isomenndlem  41531  ovnsubaddlem1  41571  hoidmv1lelem2  41593  hoidmv1le  41595  hoidmvlelem2  41597  hoidmvle  41601  hoi2toco  41608  rrnmbl  41615  hoidifhspdmvle  41621  voncmpl  41622  hoiqssbl  41626  hspmbllem1  41627  hspmbllem2  41628  ovolval2lem  41644  ovolval5lem2  41654  ovnovollem1  41657  ovnovollem2  41658  hoimbl2  41666  vonhoire  41673  salpreimagelt  41705  salpreimalegt  41707  preimaioomnf  41716  smfres  41784  smfmullem1  41785  smflimmpt  41803  smfsupmpt  41808  smfinfmpt  41812  smflimsupmpt  41822  smfliminflem  41823  smfliminfmpt  41825  sigarcol  41840  f1oresf1o  42186  f1oresf1o2  42187  sfprmdvdsmersenne  42343  lighneallem3  42347  lighneallem4  42350  nn0onn0exALTV  42432  nnsum3primesprm  42501  nnsum4primesodd  42507  nnsum4primesoddALTV  42508  elsprel  42565  c0snmgmhm  42754  rngcifuestrc  42837  funcrngcsetc  42838  funcrngcsetcALT  42839  funcringcsetc  42875  funcringcsetcALTV2lem7  42882  funcringcsetclem7ALTV  42905  lincext3  43085  lincresunit3  43110  nn0onn0ex  43158  nnpw2pmod  43217  blennn0em1  43225  digexp  43241  dignn0ehalf  43251  nn0mulfsum  43258  eenglngeehlnmlem2  43282  rrx2vlinest  43288  line2  43297  itsclinecirc0  43307  recsec  43388  reccsc  43389  aacllem  43436  amgmlemALT  43438