Theorem eqtr2d 2796

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  3eqtrrd  2800  3eqtr2rd  2802  ifan  4535  ifor  4536  dfopif  4836  fnco  6662  fnsnfv  6969  nvocnv  7293  elovmpt3rab1  7685  onsucmin  7836  csbopeq1a  8065  fnwe2lem3  8153  oaabs2  8665  ecinxp  8820  resixpfo  8971  sbthlem3  9115  rankxpsuc  9906  fseqenlem2  10111  dfac2b  10216  isf32lem9  10446  compsscnvlem  10455  ttukeylem7  10600  fpwwe2lem10  10732  00id  11492  submul2  11763  mulsubfacd  11784  divadddiv  12039  infrenegsup  12307  xadd4d  13440  fzdifsuc  13725  fzval3  13876  fzoshftral  13929  ceim1l  13994  fldiv  14007  flmod  14032  intfrac  14033  modcyc2  14054  modaddb  14056  moddi  14089  uzrdgfni  14108  axdc4uzlem  14133  seqf1olem1  14191  seqf1olem2  14192  seqid2  14198  expnegz  14246  binom2sub  14371  binom3  14375  hashreshashfun  14591  ccatw2s1p2  14793  ccats1pfxeq  14871  pfxccatin12lem2  14888  pfxccatin12  14890  swrdccat3b  14897  swrdrevpfx  14926  cshweqrep  14980  2cshwcshw  14984  ccatco  14994  swrds2  15100  relexpsucnnr  15187  relexpaddnn  15213  sgnmul  15269  reim  15285  mulre  15297  addcj  15324  absimle  15485  clim2ser  15831  isercoll2  15845  serf0  15857  iseralt  15861  summolem3  15889  isumclim3  15934  mptfzshft  15953  fsumrev  15954  fsum2mul  15964  incexc  16015  isumsplit  16018  mertenslem1  16062  fprodrev  16153  iprodclim3  16176  binomfallfaclem2  16215  ef4p  16290  tanval3  16311  efival  16329  sinmul  16349  bitsinvp1  16628  sadaddlem  16645  bitsshft  16654  smu01lem  16664  dfgcd2  16728  lcmgcdlem  16790  lcm1  16794  lcmfass  16830  eulerthlem2  16968  hashgcdeq  16976  powm2modprm  16990  pythagtriplem16  17017  pczpre  17034  pcqdiv  17044  pcadd  17076  pcfac  17086  prmreclem5  17107  4sqlem10  17134  4sqlem19  17150  vdwapun  17161  vdwlem1  17168  ramcl  17216  setsstruct  17363  strfvd  17387  strfv2d  17388  xpsff1o  17748  xpsrnbas  17752  2oppccomf  17908  oppcepi  17923  sscfn1  18001  sscfn2  18002  invfuc  18161  funcestrcsetclem7  18329  funcsetcestrclem7  18344  gsumsplit1r  18885  grpinvssd  19236  grpinvval2  19242  cycsubggend  19429  pmtrdifwrdellem2  19705  psgnunilem1  19716  psgnuni  19722  pgp0  19819  sylow1lem1  19821  sylow3lem2  19851  efgredleme  19966  efgcpbllemb  19978  frgpuptinv  19994  frgpup3lem  20000  gexexlem  20075  cyggenod  20107  gsumval3eu  20127  gsumval3  20130  gsumzaddlem  20144  dprd2db  20268  ablsimpgfindlem1  20332  ringinvdv  20653  c0snmgmhm  20701  rngcifuestrc  20900  funcrngcsetc  20901  funcrngcsetcALT  20902  funcringcsetc  20935  lss1d  21247  pwssplit1  21343  rhmqusnsg  21590  rngqiprnglin  21607  znzrh2  21860  regsumsupp  21937  ipassr2  21962  dsmmfi  22053  frlmlss  22066  frlmip  22093  frlmlbs  22112  frlmup3  22115  islindf4  22153  mplcoe3  22356  subrgascl  22384  evlseu  22401  psdadd  22493  ply1sclid  22616  ply1chr  22633  evls1addd  22698  evls1muld  22699  evls1vsca  22700  evls1maprhm  22703  evls1maplmhm  22704  evls1maprnss  22705  evl1maprhm  22706  1marepvmarrepid  22899  madurid  22968  smadiadetlem3  22992  matunitlindflem1  23003  matunitlindflem2  23004  mat2pmatghm  23057  pmatcollpwscmatlem1  23116  pm2mpmhmlem2  23146  cpmadurid  23194  cpmidgsumm2pm  23196  cpmadugsumlemB  23201  cayhamlem2  23211  ntrval2  23378  ordtuni  23517  cnclima  23595  cmpsub  23727  ptbasfi  23909  txbasval  23934  pt1hmeo  24134  alexsubALTlem1  24375  trust  24557  ussid  24588  ressuss  24590  ressprdsds  24699  imasdsf1olem  24701  setsms  24808  tmsxms  24814  tmsxpsmopn  24865  subgnm  24961  tngnm  24979  tngngp2  24980  xrsxmet  25138  xrge0gsumle  25162  metdstri  25180  xrhmeo  25276  lebnumlem3  25293  pcorevlem  25356  pi1xfrcnvlem  25386  clmabs  25413  cvsmuleqdivd  25464  rrxip  25720  rrxds  25723  rrxdsfi  25741  minveclem4a  25760  pjthlem1  25767  divcncf  25777  ovolunlem1a  25826  mbfres2  25975  i1faddlem  26023  ibladdlem  26149  iblabs  26158  ditgsplit  26190  dvmptresicc  26245  dvnres  26260  dvmptdiv  26303  dveflem  26308  dveq0  26329  dvfsumabs  26352  itgsubstlem  26377  ply1divex  26464  r1pid2  26489  dgrco  26603  plycjlem  26604  taylthlem1  26709  pserdv2  26766  abelthlem6  26772  abelthlem7  26774  tangtx  26843  abssinper  26858  sineq0  26861  explog  26931  reexplog  26932  eflogeq  26939  abslogle  26955  tanarg  26956  logtayl  26997  logtayl2  26999  relogbdiv  27116  ang180lem3  27148  affineequiv  27160  affineequiv2  27161  chordthmlem4  27172  chordthmlem5  27173  heron  27175  dcubic1lem  27180  dcubic2  27181  dcubic  27183  mcubic  27184  cubic2  27185  dquartlem1  27188  dquart  27190  quart1lem  27192  quartlem1  27194  quart  27198  acoscos  27230  atanlogaddlem  27250  atantayl2  27275  atantayl3  27276  birthdaylem2  27289  efrlim  27306  amgmlem  27326  logdifbnd  27330  emcllem3  27334  emcllem6  27337  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamgulmlem4  27368  lgamgulmlem5  27369  gamigam  27389  lgamcvg2  27391  gamfac  27403  basellem3  27419  basellem8  27424  basellem9  27425  chtprm  27489  logfaclbnd  27558  perfect1  27564  bcp1ctr  27615  bclbnd  27616  bposlem1  27620  lgsdilem  27660  lgsdirnn0  27680  lgsdinn0  27681  gausslemma2dlem1a  27701  gausslemma2dlem4  27705  gausslemma2dlem5a  27706  lgseisenlem2  27712  lgsquadlem1  27716  2sqlem2  27754  mul2sq  27755  2sqmod  27772  2sqnn0  27774  vmadivsum  27818  rpvmasumlem  27823  dchrisumlem1  27825  dchrisumlem2  27826  dchrmusum2  27830  dchrvmasum2if  27833  dchrisum0lem2  27854  logsqvma2  27879  selberg3  27895  selberg4lem1  27896  pntrsumo1  27901  pntrlog2bndlem2  27914  pntrlog2bndlem3  27915  pntrlog2bndlem5  27917  pntibndlem2  27927  pntlemk  27942  pntlemo  27943  ostth2lem4  27972  ostth3  27974  flt4lem7  27998  subsfo  28460  negsval2  28461  ltonold  28656  noseqrdgfn  28701  n0fincut  28750  addhalfcut  28854  bdayfinbndlem1  28862  z12shalf  28875  tgbtwndiff  28978  tgifscgr  28980  trgcgrg  28987  motcgr3  29017  tgbtwnconn1lem1  29044  tgbtwnconn1lem2  29045  ismir  29140  miriso  29151  midexlem  29173  symquadprlnglem  29174  ragmir  29184  footexALT  29202  footexlem1  29203  footexlem2  29204  colperpexlem3  29217  mideulem2  29219  midex  29222  opphllem3  29234  midcgr  29294  lmiisolem  29310  prlngmid2  29448  quadcgrprlng  29453  brbtwn2  29492  colinearalglem4  29496  axsegconlem1  29504  axpaschlem  29527  axcontlem4  29554  axcontlem7  29557  axcontlem8  29558  ushgredgedgloop  29821  pfxwlk  30275  crctcshwlkn0lem6  30413  wwlknlsw  30445  wwlksnextwrd  30495  clwlkclwwlklem2a3  30594  clwlkclwwlk2  30603  clwwlkel  30646  clwwlkfo  30650  clwwlkext2edg  30656  eupth2eucrct  30827  numclwwlk2lem1lem  30952  numclwwlk1lem2fo  30968  numclwlk2lem2f  30987  grpoidinvlem2  31116  nvmtri  31282  cnnvm  31293  nvnd  31299  ipidsq  31321  ipnm  31322  ipipcj  31326  blocnilem  31415  ipasslem2  31443  dipsubdir  31459  hvaddsubval  31644  pjhthlem1  32002  pjspansn  32188  pjo  32282  unoplin  32531  adjadj  32547  hmoplin  32553  eigvec1  32573  lnopeqi  32619  nmcexi  32637  lnfnsubi  32657  riesz3i  32673  kbass6  32732  leoprf2  32738  leoprf  32739  pjnmopi  32759  mdslmd1lem1  32936  mdslmd1lem2  32937  superpos  32965  ifeq3da  33193  fgreu  33316  cocnvf1o  33371  resf1o  33372  quad3d  33391  fprodex01  33466  ccatws1f1o  33564  wrdt2ind  33566  mndlactfo  33638  mndractfo  33640  gsummpt2d  33660  gsummptp1  33668  xrge0tsmseq  33686  gsumwrd2dccatlem  33688  gsumwrd2dccat  33689  symgfcoeu  33693  wrdpmtrlast  33704  psgnfzto1stlem  33711  psgnfzto1st  33716  cycpm2tr  33730  cycpmco2lem6  33742  cycpmco2lem7  33743  subrgchr  33847  elrgspnlem1  33853  elrgspnlem3  33855  elrgspnsubrunlem1  33858  rloccring  33882  rhmdvd  33935  qusrn  34010  nsgqusf1olem3  34016  rhmquskerlem  34025  elrspunsn  34029  mxidlirredi  34046  qsdrngi  34069  1arithidomlem1  34117  1arithidomlem2  34118  evls1subd  34154  deg1prod  34165  0mplrim  34196  evlextv  34224  psrmonprod  34234  esplyfval1  34255  esplyind  34257  esplyindfv  34258  esplyfvn  34259  vietalem  34261  resssra  34269  dimval  34283  dimvalfi  34284  lindsunlem  34306  dimkerim  34309  qusdimsum  34310  fedgmullem1  34311  extdg1id  34348  fldextrspunlsplem  34355  fldextrspunlsp  34356  fldextrspunlem1  34357  fldextrspundgdvds  34363  extdgfialglem1  34374  extdgfialglem2  34375  ply1annidllem  34383  algextdeglem4  34402  constrrtcc  34417  constrsslem  34423  constrresqrtcl  34459  cos9thpiminplylem2  34465  cos9thpiminply  34470  madjusmdetlem2  34510  qtophaus  34518  zarclssn  34555  zarcmplem  34563  pstmval  34577  mndpluscn  34608  qqhucn  34674  esumval  34728  gsumesum  34741  esumcst  34745  esumpcvgval  34760  oddpwdc  35036  eulerpartlemgvv  35058  probdif  35102  signsvtn  35263  actfunsnf1o  35283  reprpmtf1o  35305  hgt750lemd  35327  logdivsqrle  35329  hgt750lemg  35333  hgt750lemb  35335  bnj1415  35718  vonf1oonfo  35972  derangen2  36029  subfaclefac  36031  subfaclim  36043  satom  36211  fmla  36236  mrsubrn  36368  sinccvglem  36527  bcprod  36599  nmulss1  37059  filnetlem4  37265  curunc  38634  ltflcei  38640  poimirlem16  38663  poimirlem17  38664  poimirlem19  38666  poimirlem20  38667  poimirlem24  38671  mblfinlem4  38687  ibladdnclem  38703  iblabsnc  38711  iblmulc2nc  38712  ftc1anclem6  38725  ftc1anclem8  38727  sdclem2  38785  ismtycnv  38845  heiborlem10  38863  lflvsass  40247  lkrscss  40264  eqlkr  40265  eqlkr3  40267  ldualvsdi2  40310  omllaw3  40411  cmtcomlemN  40414  cmtbr3N  40420  omlfh3N  40425  llnexchb2lem  41034  dalawlem7  41043  dalawlem11  41047  dalawlem12  41048  pol1N  41076  paddatclN  41115  4atexlemcnd  41238  ltrncoidN  41294  cdleme3b  41395  cdleme11  41436  cdleme15a  41440  cdleme22e  41510  cdleme22g  41514  cdlemg18b  41845  trlcoat  41889  cdlemk2  41998  cdlemk4  42000  cdlemki  42007  cdlemksv2  42013  cdlemk15  42021  cdlemk55a  42125  diainN  42223  dia2dimlem3  42232  dia2dimlem5  42234  dvhlveclem  42274  diaocN  42291  cdlemn4  42364  cdlemn8  42370  dihopelvalcpre  42414  dihmeetlem9N  42481  dih1dimatlem  42495  dihpN  42502  dochvalr3  42529  dochsat  42549  djhjlj  42569  dochdmm1  42576  dihjatcclem4  42587  dihjat1  42595  dihjat4  42599  dochsnkr2cl  42640  dochfl1  42642  lclkrlem2j  42682  mapdordlem2  42803  mapdrvallem2  42811  hdmap10  43006  lcmineqlem12  43199  3lexlogpow5ineq5  43219  aks4d1p1  43235  primrootsunit1  43256  primrootscoprmpow  43258  posbezout  43259  aks6d1c1p3  43269  aks6d1c1p4  43270  aks6d1c1p5  43271  aks6d1c1p7  43272  evl1gprodd  43276  hashscontpow1  43280  aks6d1c3  43282  aks6d1c2lem3  43285  aks6d1c2lem4  43286  aks6d1c2  43289  aks6d1c5lem3  43296  aks6d1c6lem1  43329  aks6d1c6isolem3  43335  aks6d1c6lem5  43336  bcle2d  43338  aks6d1c7lem1  43339  aks5lem3a  43348  grpods  43353  unitscyglem1  43354  unitscyglem2  43355  unitscyglem4  43357  unitscyglem5  43358  aks5lem7  43359  nicomachus  43478  sumcubes  43479  cnreeu  43663  frlmvscadiccat  43682  grpcominv1  43684  riccrng1  43691  ricdrng1  43701  frlmsnic  43713  evlselv  43726  fsuppind  43727  negexpidd  43801  3cubeslem2  43804  3cubeslem3r  43806  mzpsubmpt  43863  irrapxlem3  43940  pellexlem6  43950  pell1234qrne0  43969  pell1234qrreccl  43970  pell1234qrmulcl  43971  pell14qrdich  43985  pell1qrgaplem  43989  rmxluc  44052  rmyluc  44053  jm2.24nn  44075  jm2.18  44104  jm2.19lem2  44106  jm2.19lem3  44107  jm2.22  44111  jm2.23  44112  jm2.16nn0  44120  jm2.27c  44123  lmhmfgsplit  44197  hbtlem2  44235  onsucf1lem  44380  ofoafo  44467  naddcnffo  44475  naddwordnexlem4  44512  reabssgn  44745  relexpmulnn  44818  relexpmulg  44819  ntrclsneine0lem  45173  int-addassocd  45283  dvconstbi  45427  bccm1k  45435  binomcxplemnotnn0  45449  fmptsnxp  46292  wessf1ornlem  46308  projf1o  46319  infnsuprnmpt  46370  lefldiveq  46416  lt4addmuld  46430  fzdifsuc2  46434  suplesup  46459  infrpge  46471  xrlexaddrp  46472  xralrple2  46474  infleinflem1  46489  supminfrnmpt  46563  supminfxr2  46587  fsumnncl  46692  limcperiod  46748  sumnnodd  46750  limcresiooub  46760  limcresioolb  46761  0ellimcdiv  46767  reclimc  46771  limsupval3  46810  limsupequzmpt2  46836  liminfval5  46883  limsupresxr  46884  liminfresxr  46885  liminfvalxr  46901  liminfequzmpt2  46909  climliminflimsupd  46919  liminfltlem  46922  liminflbuz2  46933  sinmulcos  46983  coskpi2  46984  cncfdmsn  47008  cncfiooicclem1  47011  fprodsubrecnncnvlem  47025  fprodaddrecnncnvlem  47027  fperdvper  47037  dvnmptdivc  47056  dvnxpaek  47060  dvnmul  47061  dvnprodlem1  47064  dvnprodlem3  47066  itgcoscmulx  47087  itgsincmulx  47092  itgspltprt  47097  itgiccshift  47098  itgperiod  47099  sublevolico  47102  volioof  47105  ovolsplit  47106  fvvolioof  47107  fvvolicof  47109  stoweidlem22  47140  stoweidlem32  47150  wallispilem5  47187  stirlinglem5  47196  dirkertrigeqlem2  47217  dirkertrigeq  47219  dirkercncflem1  47221  dirkercncflem2  47222  dirkercncflem4  47224  fourierdlem13  47238  fourierdlem16  47241  fourierdlem19  47244  fourierdlem21  47246  fourierdlem22  47247  fourierdlem28  47253  fourierdlem32  47257  fourierdlem33  47258  fourierdlem42  47267  fourierdlem47  47271  fourierdlem48  47272  fourierdlem49  47273  fourierdlem50  47274  fourierdlem56  47280  fourierdlem60  47284  fourierdlem61  47285  fourierdlem64  47288  fourierdlem66  47290  fourierdlem71  47295  fourierdlem73  47297  fourierdlem74  47298  fourierdlem76  47300  fourierdlem78  47302  fourierdlem79  47303  fourierdlem80  47304  fourierdlem81  47305  fourierdlem83  47307  fourierdlem88  47312  fourierdlem92  47316  fourierdlem93  47317  fourierdlem97  47321  fourierdlem101  47325  fourierdlem103  47327  fourierdlem104  47328  fourierdlem109  47333  fourierdlem111  47335  fouriersw  47349  elaa2lem  47351  etransclem24  47376  etransclem25  47377  etransclem35  47387  etransclem46  47398  rrndistlt  47408  rrxunitopnfi  47410  qndenserrnbl  47413  qndenserrnopnlem  47415  saldifcl2  47446  intsal  47448  sge0sn  47497  sge0ltfirp  47518  sge0iunmptlemre  47533  sge0fodjrnlem  47534  sge0isum  47545  sge0xaddlem1  47551  nnfoctbdjlem  47573  meassle  47581  ismeannd  47585  meadif  47597  meaiuninclem  47598  meaiininclem  47604  omeunile  47623  caragendifcl  47632  caratheodory  47646  isomenndlem  47648  ovnsubaddlem1  47688  hoidmv1lelem2  47710  hoidmv1le  47712  hoidmvlelem2  47714  hoidmvle  47718  hoi2toco  47725  rrnmbl  47732  hoidifhspdmvle  47738  voncmpl  47739  hoiqssbl  47743  hspmbllem1  47744  hspmbllem2  47745  ovolval2lem  47761  ovolval5lem2  47771  ovnovollem1  47774  ovnovollem2  47775  hoimbl2  47783  vonhoire  47790  salpreimagelt  47825  salpreimalegt  47827  preimaioomnf  47837  smfres  47908  smfmullem1  47909  smflimmpt  47928  smfsupmpt  47933  smfinfmpt  47937  smflimsupmpt  47947  smfliminflem  47948  smfliminfmpt  47950  sigarcol  47982  sin5tlem2  48028  sinnpoly  48049  sqrtnpoly  48051  f1oresf1o  48468  elsprel  48665  prproropf1o  48697  paireqne  48701  sfprmdvdsmersenne  48796  lighneallem3  48800  lighneallem4  48803  nprmdvdsfacm1lem1  48813  nn0onn0exALTV  48905  nnsum3primesprm  48996  nnsum4primesodd  49002  nnsum4primesoddALTV  49003  isuspgrim0lem  49099  clnbgrgrimlem  49139  uspgrlimlem3  49196  uspgrlimlem4  49197  gpgedgvtx0  49267  gpgedgvtx1  49268  funcringcsetcALTV2lem7  49501  funcringcsetclem7ALTV  49524  lincext3  49676  lincresunit3  49701  nn0onn0ex  49743  nnpw2pmod  49803  blennn0em1  49811  digexp  49827  dignn0ehalf  49837  nn0mulfsum  49844  itcovalpclem1  49890  eenglngeehlnmlem2  49959  rrx2vlinest  49961  line2  49972  itschlc0xyqsol  49987  itsclinecirc0b  49994  toplatjoin  50224  toplatmeet  50225  upeu2lem  50250  oppff1o  50373  imaf1co  50379  upciclem3  50392  natoppfb  50461  oppcthinco  50682  oppcthinendcALT  50684  lmddu  50958  recsec  51032  reccsc  51033  aacllem  51122  crossp3d  51150  amgmlemALT  51171