Theorem eqtr3i 2646

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)

Hypotheses

Ref	Expression
eqtr3i.1	|- A = B
eqtr3i.2	|- A = C

Assertion

Ref	Expression
eqtr3i	|- B = C

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 |- A = B
2	1	eqcomi 2631	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2644	1 |- B = C

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  3eqtr3i  2652  3eqtr3ri  2653  unundi  3774  unundir  3775  inindi  3830  inindir  3831  dfin4  3867  difun1  3887  difabs  3892  notab  3897  dif0  3950  difdifdir  4056  tpidm13  4291  intmin2  4504  iunxdif3  4606  univ  4919  iunxpconst  5175  dmres  5419  opabresid  5455  rnresi  5479  cnvcnvOLD  5587  rnresv  5594  cnvsn0  5603  cnvsn  5618  resdmres  5625  coi2  5652  coires1  5653  dfdm2  5667  isarep2  5978  resasplit  6074  ssimaex  6263  fnreseql  6327  resfunexg  6479  idref  6499  mpt2mpt  6752  caov31  6863  fvresex  7139  xpexgALT  7161  1st2val  7194  2nd2val  7195  fnsuppeq0  7323  ecopovtrn  7850  limensuci  8136  pssnn  8178  r1sucg  8632  jech9.3  8677  rankbnd2  8732  compss  9198  zorn2lem4  9321  iunfo  9361  cardf  9372  alephsuc3  9402  fpwwe2lem13  9464  rankcf  9599  halfnq  9798  addclprlem2  9839  mulgt0sr  9926  mul02lem2  10213  mul02  10214  addid1  10216  mvlladdi  10299  mvllmuli  10858  infrenegsup  11006  8th4div3  11252  nneo  11461  dec10OLD  11555  nummac  11558  numadd  11560  numaddc  11561  nummul1c  11562  9p2e11OLD  11620  decbin0  11682  rpsup  12665  resup  12666  om2uzrdg  12755  m1expcl2  12882  facnn  13062  fac0  13063  faclbnd4lem1  13080  4bc3eq4  13115  hasheq0  13154  f1oun2prg  13662  sqrt1  14012  sqrt4  14013  sqrt9  14014  rddif  14080  abs3lemi  14149  sumss2  14457  divcnvshft  14587  geo2sum2  14605  geomulcvg  14607  geoihalfsum  14614  risefall0lem  14757  bpoly2  14788  bpoly3  14789  sin0  14879  efival  14882  ef01bndlem  14914  cos2bnd  14918  sin4lt0  14925  flodddiv4  15137  2prm  15405  unbenlem  15612  dec5dvds  15768  modxai  15772  mod2xi  15773  mod2xnegi  15775  gcdi  15777  numexp2x  15783  decsplit  15787  decsplitOLD  15791  setsid  15914  mreexexlem3d  16306  oppchom  16375  2oppchomf  16384  isoval  16425  estrres  16779  oppchofcl  16900  oyoncl  16910  mvdco  17865  m1expaddsub  17918  psgn0fv0  17931  oppglsm  18057  dprd2da  18441  ring1  18602  opprsubg  18636  lsppratlem1  19147  opsrtoslem1  19484  ply1basfvi  19611  coe1tm  19643  ply1coe  19666  zzngim  19901  cnmsgnsubg  19923  psgninv  19928  zrhpsgnmhm  19930  neitr  20984  comppfsc  21335  kgeni  21340  xkoinjcn  21490  ufprim  21713  metreslem  22167  restmetu  22375  retopbas  22564  cnfldms  22579  qdensere2  22600  xrsmopn  22615  metdscn2  22660  pcoass  22824  recvs  22946  zclmncvs  22948  iscmet3lem3  23088  cncms  23151  cnfldcusp  23153  resscdrg  23154  rrxprds  23177  ovoliunnul  23275  uniioombllem4  23354  vitalilem5  23381  mbfres  23411  ismbf3d  23421  i1fima  23445  i1fd  23448  itg2cnlem1  23528  itgss3  23581  ellimc2  23641  limccnp2  23656  cpnres  23700  lhop  23779  plyeq0  23967  plypf1  23968  sinhalfpilem  24215  sincos6thpi  24267  sincos3rdpi  24268  pige3  24269  dfrelog  24312  logimul  24360  logneg2  24361  dvlog  24397  cxpsqrt  24449  ang180lem2  24540  ang180lem3  24541  ang180lem4  24542  quart1  24583  asin1  24621  atan0  24635  atanlogsublem  24642  atan1  24655  log2tlbnd  24672  log2ublem2  24674  log2ub  24676  basellem8  24814  cht2  24898  ppiub  24929  bposlem6  25014  bposlem8  25016  bposlem9  25017  lgsdir2lem3  25052  lgseisenlem1  25100  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  2lgsoddprmlem2  25134  chebbnd1  25161  istrkg3ld  25360  tgcgr4  25426  motplusg  25437  ax5seglem7  25815  ex-un  27281  ex-sqrt  27311  ipdirilem  27684  ipasslem10  27694  hisubcomi  27961  normlem0  27966  norm3difi  28004  norm3lem  28006  polid2i  28014  chdmj1i  28340  chjjdiri  28383  spansn0  28400  pjoml4i  28446  cmbr3i  28459  qlaxr3i  28495  honpcani  28684  honpncani  28686  lnopunilem1  28869  lnophmlem2  28876  lnfn0i  28901  pjbdlni  29008  pjclem1  29054  pjclem3  29056  pjci  29059  atomli  29241  atabs2i  29261  mddmdin0i  29290  difeq  29355  disjdifprg  29388  imadifxp  29414  fnresin  29430  ofpreima2  29466  df1stres  29481  df2ndres  29482  cnvoprab  29498  dfdec100  29576  decdiv10  29604  dpmul100  29605  dpmul1000  29607  dpexpp1  29616  dpadd2  29618  dpadd  29619  dpmul  29621  dpmul4  29622  threehalves  29623  xrge0base  29685  xrge00  29686  xrge0mulgnn0  29689  xrge0slmod  29844  lmatfvlem  29881  xrge0iifcnv  29979  lmxrge0  29998  cnrrext  30054  qqtopn  30055  esumrnmpt2  30130  esumpfinvallem  30136  unelldsys  30221  ldgenpisyslem1  30226  measunl  30279  mbfmcst  30321  difelcarsg  30372  carsggect  30380  sibfof  30402  eulerpartlemmf  30437  fib2  30464  fib3  30465  fib4  30466  fib5  30467  fib6  30468  0rrv  30513  coinfliprv  30544  ballotlem2  30550  prodfzo03  30681  chtvalz  30707  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  kur14lem6  31193  kur14lem7  31194  cvmlift2lem12  31296  problem5  31563  quad3  31564  divcnvlin  31618  logi  31620  bj-2upln1upl  33012  bj-rest0  33046  relowlssretop  33211  relowlpssretop  33212  1oequni2o  33216  curunc  33391  ptrest  33408  poimirlem16  33425  poimirlem30  33439  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  itg2addnclem2  33462  ftc1anclem5  33489  ftc1anclem6  33490  sdc  33540  heiborlem3  33612  dvh4dimN  36736  dnnumch1  37614  aomclem6  37629  areaquad  37802  unitadd  38498  seff  38508  sblpnf  38509  hashnzfz  38519  lhe4.4ex1a  38528  xrtgcntopre  39709  iccdifioo  39741  itgsin0pilem1  40165  stoweidlem13  40230  stoweidlem26  40243  fourierdlem62  40385  fourierdlem102  40425  fourierdlem114  40437  fourierswlem  40447  fouriersw  40448  sge0tsms  40597  meaiuninc  40698  fmtno4prmfac  41484  41prothprm  41536  2zrngasgrp  41940  2zrngmsgrp  41947  mvlraddi  42514  mvlrmuli  42523  i2linesi  42524