Theorem eqtr2d 2771

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  3eqtrrd  2775  3eqtr2rd  2777  ifan  4554  ifor  4555  dfopif  4846  fnco  6655  fnsnfv  6957  nvocnv  7273  elovmpt3rab1  7665  onsucmin  7813  csbopeq1a  8047  oaabs2  8659  ecinxp  8804  resixpfo  8948  sbthlem3  9097  rankxpsuc  9894  fseqenlem2  10037  dfac2b  10143  isf32lem9  10373  compsscnvlem  10382  ttukeylem7  10527  fpwwe2lem10  10652  00id  11408  submul2  11675  mulsubfacd  11696  divadddiv  11954  infrenegsup  12223  xadd4d  13317  fzdifsuc  13599  fzval3  13748  fzoshftral  13798  ceim1l  13862  fldiv  13875  flmod  13900  intfrac  13901  modcyc2  13922  moddi  13955  uzrdgfni  13974  axdc4uzlem  13999  seqf1olem1  14057  seqf1olem2  14058  seqid2  14064  expnegz  14112  binom2sub  14236  binom3  14240  hashreshashfun  14455  ccatw2s1p2  14653  ccats1pfxeq  14730  pfxccatin12lem2  14747  pfxccatin12  14749  swrdccat3b  14756  cshweqrep  14837  2cshwcshw  14842  ccatco  14852  swrds2  14957  relexpsucnnr  15042  relexpaddnn  15068  reim  15126  mulre  15138  addcj  15165  absimle  15326  clim2ser  15669  isercoll2  15683  serf0  15695  iseralt  15699  summolem3  15728  isumclim3  15773  mptfzshft  15792  fsumrev  15793  fsum2mul  15803  incexc  15851  isumsplit  15854  mertenslem1  15898  fprodrev  15991  iprodclim3  16014  binomfallfaclem2  16054  ef4p  16129  tanval3  16150  efival  16168  sinmul  16188  bitsinvp1  16466  sadaddlem  16483  bitsshft  16492  smu01lem  16502  dfgcd2  16563  lcmgcdlem  16623  lcm1  16627  lcmfass  16663  eulerthlem2  16799  hashgcdeq  16807  powm2modprm  16821  pythagtriplem16  16848  pczpre  16865  pcqdiv  16875  pcadd  16907  pcfac  16917  prmreclem5  16938  4sqlem10  16965  4sqlem19  16981  vdwapun  16992  vdwlem1  16999  ramcl  17047  setsstruct  17193  strfvd  17217  strfv2d  17218  xpsff1o  17579  xpsrnbas  17583  2oppccomf  17735  oppcepi  17750  sscfn1  17828  sscfn2  17829  invfuc  17988  funcestrcsetclem7  18156  funcsetcestrclem7  18171  gsumsplit1r  18663  grpinvssd  18998  grpinvval2  19004  cycsubggend  19186  pmtrdifwrdellem2  19461  psgnunilem1  19472  psgnuni  19478  pgp0  19575  sylow1lem1  19577  sylow3lem2  19607  efgredleme  19722  efgcpbllemb  19734  frgpuptinv  19750  frgpup3lem  19756  gexexlem  19831  cyggenod  19863  gsumval3eu  19883  gsumval3  19886  gsumzaddlem  19900  dprd2db  20024  ablsimpgfindlem1  20088  ringinvdv  20372  c0snmgmhm  20420  rngcifuestrc  20597  funcrngcsetc  20598  funcrngcsetcALT  20599  funcringcsetc  20632  lss1d  20918  pwssplit1  21015  rhmqusnsg  21244  rngqiprnglin  21261  znzrh2  21504  regsumsupp  21580  ipassr2  21605  dsmmfi  21696  frlmlss  21709  frlmip  21736  frlmlbs  21755  frlmup3  21758  islindf4  21796  mplcoe3  21994  subrgascl  22022  evlseu  22039  psdadd  22099  ply1sclid  22223  ply1chr  22242  evls1addd  22307  evls1muld  22308  evls1vsca  22309  evls1maprhm  22312  evls1maplmhm  22313  evls1maprnss  22314  evl1maprhm  22315  1marepvmarrepid  22511  madurid  22580  smadiadetlem3  22604  mat2pmatghm  22666  pmatcollpwscmatlem1  22725  pm2mpmhmlem2  22755  cpmadurid  22803  cpmidgsumm2pm  22805  cpmadugsumlemB  22810  cayhamlem2  22820  ntrval2  22987  ordtuni  23126  cnclima  23204  cmpsub  23336  ptbasfi  23517  txbasval  23542  pt1hmeo  23742  alexsubALTlem1  23983  trust  24166  ussid  24197  ressuss  24199  ressprdsds  24308  imasdsf1olem  24310  setsms  24417  tmsxms  24423  tmsxpsmopn  24474  subgnm  24570  tngnm  24588  tngngp2  24589  xrsxmet  24747  xrge0gsumle  24771  metdstri  24789  xrhmeo  24893  lebnumlem3  24911  pcorevlem  24975  pi1xfrcnvlem  25005  clmabs  25032  cvsmuleqdivd  25083  rrxip  25340  rrxds  25343  rrxdsfi  25361  minveclem4a  25380  pjthlem1  25387  divcncf  25398  ovolunlem1a  25447  mbfres2  25596  i1faddlem  25644  ibladdlem  25771  iblabs  25780  ditgsplit  25812  dvmptresicc  25867  dvnres  25883  dvmptdiv  25928  dveflem  25933  dveq0  25955  dvfsumabs  25979  itgsubstlem  26005  ply1divex  26092  r1pid2  26117  dgrco  26231  plycjlem  26232  taylthlem1  26331  pserdv2  26390  abelthlem6  26396  abelthlem7  26398  tangtx  26464  abssinper  26480  sineq0  26483  explog  26553  reexplog  26554  eflogeq  26561  abslogle  26577  tanarg  26578  logtayl  26619  logtayl2  26621  relogbdiv  26739  ang180lem3  26771  affineequiv  26783  affineequiv2  26784  chordthmlem4  26795  chordthmlem5  26796  heron  26798  dcubic1lem  26803  dcubic2  26804  dcubic  26806  mcubic  26807  cubic2  26808  dquartlem1  26811  dquart  26813  quart1lem  26815  quartlem1  26817  quart  26821  acoscos  26853  atanlogaddlem  26873  atantayl2  26898  atantayl3  26899  birthdaylem2  26912  efrlim  26929  efrlimOLD  26930  amgmlem  26950  logdifbnd  26954  emcllem3  26958  emcllem6  26961  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  gamigam  27013  lgamcvg2  27015  gamfac  27027  basellem3  27043  basellem8  27048  basellem9  27049  chtprm  27113  logfaclbnd  27183  perfect1  27189  bcp1ctr  27240  bclbnd  27241  bposlem1  27245  lgsdilem  27285  lgsdirnn0  27305  lgsdinn0  27306  gausslemma2dlem1a  27326  gausslemma2dlem4  27330  gausslemma2dlem5a  27331  lgseisenlem2  27337  lgsquadlem1  27341  2sqlem2  27379  mul2sq  27380  2sqmod  27397  2sqnn0  27399  vmadivsum  27443  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem2  27451  dchrmusum2  27455  dchrvmasum2if  27458  dchrisum0lem2  27479  logsqvma2  27504  selberg3  27520  selberg4lem1  27521  pntrsumo1  27526  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem5  27542  pntibndlem2  27552  pntlemk  27567  pntlemo  27568  ostth2lem4  27597  ostth3  27599  subsfo  28012  negsval2  28013  sltonold  28200  noseqrdgfn  28229  addhalfcut  28336  tgbtwndiff  28431  tgifscgr  28433  trgcgrg  28440  motcgr3  28470  tgbtwnconn1lem1  28497  tgbtwnconn1lem2  28498  ismir  28584  miriso  28595  midexlem  28617  ragmir  28625  footexALT  28643  footexlem1  28644  footexlem2  28645  colperpexlem3  28657  mideulem2  28659  midex  28662  opphllem3  28674  midcgr  28705  lmiisolem  28721  brbtwn2  28830  colinearalglem4  28834  axsegconlem1  28842  axpaschlem  28865  axcontlem4  28892  axcontlem7  28895  axcontlem8  28896  ushgredgedgloop  29156  crctcshwlkn0lem6  29743  wwlknlsw  29775  wwlksnextwrd  29825  clwlkclwwlklem2a3  29921  clwlkclwwlk2  29930  clwwlkel  29973  clwwlkfo  29977  clwwlkext2edg  29983  eupth2eucrct  30144  numclwwlk2lem1lem  30269  numclwwlk1lem2fo  30285  numclwlk2lem2f  30304  grpoidinvlem2  30432  nvmtri  30598  cnnvm  30609  nvnd  30615  ipidsq  30637  ipnm  30638  ipipcj  30642  blocnilem  30731  ipasslem2  30759  dipsubdir  30775  hvaddsubval  30960  pjhthlem1  31318  pjspansn  31504  pjo  31598  unoplin  31847  adjadj  31863  hmoplin  31869  eigvec1  31889  lnopeqi  31935  nmcexi  31953  lnfnsubi  31973  riesz3i  31989  kbass6  32048  leoprf2  32054  leoprf  32055  pjnmopi  32075  mdslmd1lem1  32252  mdslmd1lem2  32253  superpos  32281  ifeq3da  32473  fgreu  32596  resf1o  32653  quad3d  32673  fprodex01  32750  sgnmul  32760  ccatws1f1o  32873  wrdt2ind  32875  mndlactfo  32968  mndractfo  32970  gsummpt2d  32989  xrge0tsmseq  33004  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  symgfcoeu  33039  wrdpmtrlast  33050  psgnfzto1stlem  33057  psgnfzto1st  33062  cycpm2tr  33076  cycpmco2lem6  33088  cycpmco2lem7  33089  subrgchr  33178  elrgspnlem1  33183  elrgspnlem3  33185  elrgspnsubrunlem1  33188  rloccring  33211  rhmdvd  33286  qusrn  33370  nsgqusf1olem3  33376  rhmquskerlem  33386  elrspunsn  33390  mxidlirredi  33432  qsdrngi  33456  1arithidomlem1  33496  1arithidomlem2  33497  evls1subd  33531  r1pid2OLD  33564  resssra  33573  dimval  33586  dimvalfi  33587  lindsunlem  33610  dimkerim  33613  qusdimsum  33614  fedgmullem1  33615  extdg1id  33653  fldextrspunlsplem  33660  fldextrspunlsp  33661  fldextrspunlem1  33662  fldextrspundgdvds  33668  ply1annidllem  33681  algextdeglem4  33700  constrrtcc  33715  constrsslem  33721  constrresqrtcl  33757  cos9thpiminplylem2  33763  cos9thpiminply  33768  madjusmdetlem2  33805  qtophaus  33813  zarclssn  33850  zarcmplem  33858  pstmval  33872  mndpluscn  33903  qqhucn  33969  esumval  34023  gsumesum  34036  esumcst  34040  esumpcvgval  34055  oddpwdc  34332  eulerpartlemgvv  34354  probdif  34398  signsvtn  34562  actfunsnf1o  34582  reprpmtf1o  34604  hgt750lemd  34626  logdivsqrle  34628  hgt750lemg  34632  hgt750lemb  34634  bnj1415  35015  swrdrevpfx  35085  pfxwlk  35092  derangen2  35142  subfaclefac  35144  subfaclim  35156  satom  35324  fmla  35349  mrsubrn  35481  sinccvglem  35640  bcprod  35701  filnetlem4  36345  curunc  37572  ltflcei  37578  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem24  37614  mblfinlem4  37630  ibladdnclem  37646  iblabsnc  37654  iblmulc2nc  37655  ftc1anclem6  37668  ftc1anclem8  37670  sdclem2  37712  ismtycnv  37772  heiborlem10  37790  lflvsass  39045  lkrscss  39062  eqlkr  39063  eqlkr3  39065  ldualvsdi2  39108  omllaw3  39209  cmtcomlemN  39212  cmtbr3N  39218  omlfh3N  39223  llnexchb2lem  39833  dalawlem7  39842  dalawlem11  39846  dalawlem12  39847  pol1N  39875  paddatclN  39914  4atexlemcnd  40037  ltrncoidN  40093  cdleme3b  40194  cdleme11  40235  cdleme15a  40239  cdleme22e  40309  cdleme22g  40313  cdlemg18b  40644  trlcoat  40688  cdlemk2  40797  cdlemk4  40799  cdlemki  40806  cdlemksv2  40812  cdlemk15  40820  cdlemk55a  40924  diainN  41022  dia2dimlem3  41031  dia2dimlem5  41033  dvhlveclem  41073  diaocN  41090  cdlemn4  41163  cdlemn8  41169  dihopelvalcpre  41213  dihmeetlem9N  41280  dih1dimatlem  41294  dihpN  41301  dochvalr3  41328  dochsat  41348  djhjlj  41368  dochdmm1  41375  dihjatcclem4  41386  dihjat1  41394  dihjat4  41398  dochsnkr2cl  41439  dochfl1  41441  lclkrlem2j  41481  mapdordlem2  41602  mapdrvallem2  41610  hdmap10  41805  lcmineqlem12  41999  3lexlogpow5ineq5  42019  aks4d1p1  42035  primrootsunit1  42056  primrootscoprmpow  42058  posbezout  42059  aks6d1c1p3  42069  aks6d1c1p4  42070  aks6d1c1p5  42071  aks6d1c1p7  42072  evl1gprodd  42076  hashscontpow1  42080  aks6d1c3  42082  aks6d1c2lem3  42085  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5lem3  42096  aks6d1c6lem1  42129  aks6d1c6isolem3  42135  aks6d1c6lem5  42136  bcle2d  42138  aks6d1c7lem1  42139  aks5lem3a  42148  grpods  42153  unitscyglem1  42154  unitscyglem2  42155  unitscyglem4  42157  unitscyglem5  42158  aks5lem7  42159  nicomachus  42308  sumcubes  42309  cnreeu  42460  frlmvscadiccat  42476  grpcominv1  42478  riccrng1  42491  ricdrng1  42498  frlmsnic  42510  evlselv  42557  fsuppind  42560  flt4lem7  42629  negexpidd  42652  3cubeslem2  42655  3cubeslem3r  42657  mzpsubmpt  42713  irrapxlem3  42794  pellexlem6  42804  pell1234qrne0  42823  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell14qrdich  42839  pell1qrgaplem  42843  rmxluc  42907  rmyluc  42908  jm2.24nn  42930  jm2.18  42959  jm2.19lem2  42961  jm2.19lem3  42962  jm2.22  42966  jm2.23  42967  jm2.16nn0  42975  jm2.27c  42978  fnwe2lem2  43022  lmhmfgsplit  43057  hbtlem2  43095  onsucf1lem  43240  ofoafo  43327  naddcnffo  43335  naddwordnexlem4  43372  reabssgn  43607  relexpmulnn  43680  relexpmulg  43681  ntrclsneine0lem  44035  int-addassocd  44145  dvconstbi  44306  bccm1k  44314  binomcxplemnotnn0  44328  fmptsnxp  45141  wessf1ornlem  45157  projf1o  45169  infnsuprnmpt  45222  lefldiveq  45269  lt4addmuld  45283  fzdifsuc2  45287  suplesup  45314  infrpge  45326  xrlexaddrp  45327  xralrple2  45329  infleinflem1  45345  supminfrnmpt  45420  supminfxr2  45444  fsumnncl  45549  limcperiod  45605  sumnnodd  45607  limcresiooub  45619  limcresioolb  45620  0ellimcdiv  45626  reclimc  45630  limsupval3  45669  limsupequzmpt2  45695  liminfval5  45742  limsupresxr  45743  liminfresxr  45744  liminfvalxr  45760  liminfequzmpt2  45768  climliminflimsupd  45778  liminfltlem  45781  liminflbuz2  45792  sinmulcos  45842  coskpi2  45843  cncfdmsn  45867  cncfiooicclem1  45870  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  fperdvper  45896  dvnmptdivc  45915  dvnxpaek  45919  dvnmul  45920  dvnprodlem1  45923  dvnprodlem3  45925  itgcoscmulx  45946  itgsincmulx  45951  itgspltprt  45956  itgiccshift  45957  itgperiod  45958  sublevolico  45961  volioof  45964  ovolsplit  45965  fvvolioof  45966  fvvolicof  45968  stoweidlem22  45999  stoweidlem32  46009  wallispilem5  46046  stirlinglem5  46055  dirkertrigeqlem2  46076  dirkertrigeq  46078  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem13  46097  fourierdlem16  46100  fourierdlem19  46103  fourierdlem21  46105  fourierdlem22  46106  fourierdlem28  46112  fourierdlem32  46116  fourierdlem33  46117  fourierdlem42  46126  fourierdlem47  46130  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem56  46139  fourierdlem60  46143  fourierdlem61  46144  fourierdlem64  46147  fourierdlem66  46149  fourierdlem71  46154  fourierdlem73  46156  fourierdlem74  46157  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem80  46163  fourierdlem81  46164  fourierdlem83  46166  fourierdlem88  46171  fourierdlem92  46175  fourierdlem93  46176  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem109  46192  fourierdlem111  46194  fouriersw  46208  elaa2lem  46210  etransclem24  46235  etransclem25  46236  etransclem35  46246  etransclem46  46257  rrndistlt  46267  rrxunitopnfi  46269  qndenserrnbl  46272  qndenserrnopnlem  46274  saldifcl2  46305  intsal  46307  sge0sn  46356  sge0ltfirp  46377  sge0iunmptlemre  46392  sge0fodjrnlem  46393  sge0isum  46404  sge0xaddlem1  46410  nnfoctbdjlem  46432  meassle  46440  ismeannd  46444  meadif  46456  meaiuninclem  46457  meaiininclem  46463  omeunile  46482  caragendifcl  46491  caratheodory  46505  isomenndlem  46507  ovnsubaddlem1  46547  hoidmv1lelem2  46569  hoidmv1le  46571  hoidmvlelem2  46573  hoidmvle  46577  hoi2toco  46584  rrnmbl  46591  hoidifhspdmvle  46597  voncmpl  46598  hoiqssbl  46602  hspmbllem1  46603  hspmbllem2  46604  ovolval2lem  46620  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  hoimbl2  46642  vonhoire  46649  salpreimagelt  46684  salpreimalegt  46686  preimaioomnf  46696  smfres  46767  smfmullem1  46768  smflimmpt  46787  smfsupmpt  46792  smfinfmpt  46796  smflimsupmpt  46806  smfliminflem  46807  smfliminfmpt  46809  sigarcol  46841  f1oresf1o  47267  elsprel  47437  prproropf1o  47469  paireqne  47473  sfprmdvdsmersenne  47565  lighneallem3  47569  lighneallem4  47572  nn0onn0exALTV  47661  nnsum3primesprm  47752  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  isuspgrim0lem  47854  clnbgrgrimlem  47894  uspgrlimlem3  47950  uspgrlimlem4  47951  gpgedgvtx0  48013  gpgedgvtx1  48014  funcringcsetcALTV2lem7  48219  funcringcsetclem7ALTV  48242  lincext3  48380  lincresunit3  48405  nn0onn0ex  48451  nnpw2pmod  48511  blennn0em1  48519  digexp  48535  dignn0ehalf  48545  nn0mulfsum  48552  itcovalpclem1  48598  eenglngeehlnmlem2  48666  rrx2vlinest  48669  line2  48680  itschlc0xyqsol  48695  itsclinecirc0b  48702  toplatjoin  48924  toplatmeet  48925  upeu2lem  48946  imaf1co  49043  upciclem3  49051  oppcthinco  49273  oppcthinendcALT  49275  recsec  49568  reccsc  49569  aacllem  49613  amgmlemALT  49615