Theorem eqtr3i 2826

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

Hypotheses

Ref	Expression
eqtr3i.1	⊢ 𝐴 = 𝐵
eqtr3i.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3i	⊢ 𝐵 = 𝐶

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2811	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2824	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2795

This theorem is referenced by:  3eqtr3i  2832  3eqtr3ri  2833  unundi  3967  unundir  3968  inindi  4021  inindir  4022  dfin4  4063  difun1  4083  difabs  4087  notab  4092  dif0  4145  difdifdir  4246  tpidm13  4476  intmin2  4689  iunxdif3  4791  univ  5103  iunxpconst  5369  dmres  5616  opabresid  5661  rnresi  5683  cnvcnvOLD  5792  rnresv  5799  cnvsn0  5808  cnvsnOLD  5826  resdmres  5833  coi2  5860  coires1  5861  dfdm2  5875  isarep2  6183  resasplit  6283  ssimaex  6478  fnreseql  6543  idref  6629  resfunexg  6698  mpt2mpt  6976  caov31  7087  fvresex  7363  xpexgALT  7385  1st2val  7420  2nd2val  7421  cnvoprab  7456  fnsuppeq0  7552  ecopovtrn  8080  limensuci  8369  pssnn  8411  r1sucg  8873  jech9.3  8918  rankbnd2  8973  djuin  9021  compss  9477  zorn2lem4  9600  iunfo  9640  cardf  9651  alephsuc3  9681  fpwwe2lem13  9743  rankcf  9878  halfnq  10077  addclprlem2  10118  mulgt0sr  10205  mul02lem2  10492  mul02  10493  addid1  10495  mvlladdi  10578  mvllmuli  11137  infrenegsup  11285  8th4div3  11513  nneo  11721  nummac  11798  numadd  11800  numaddc  11801  nummul1c  11802  decbin0  11893  rpsup  12883  resup  12884  om2uzrdg  12973  m1expcl2  13099  facnn  13276  fac0  13277  faclbnd4lem1  13294  4bc3eq4  13329  hasheq0  13366  f1oun2prg  13880  sqrt1  14229  sqrt4  14230  sqrt9  14231  rddif  14297  abs3lemi  14366  sumss2  14674  divcnvshft  14803  geo2sum2  14821  geomulcvg  14823  geoihalfsum  14829  risefall0lem  14971  bpoly2  15002  bpoly3  15003  sin0  15093  efival  15096  ef01bndlem  15128  cos2bnd  15132  sin4lt0  15139  flodddiv4  15350  2prm  15617  unbenlem  15823  dec5dvds  15979  modxai  15983  mod2xi  15984  mod2xnegi  15986  gcdi  15988  numexp2x  15994  decsplit  15998  setsid  16119  mreexexlem3d  16505  oppchom  16573  2oppchomf  16582  isoval  16623  estrresOLD  16977  estrres  16978  oppchofcl  17099  oyoncl  17109  mvdco  18060  m1expaddsub  18113  psgn0fv0  18126  oppglsm  18252  dprd2da  18637  ring1  18798  opprsubg  18832  lsppratlem1  19350  opsrtoslem1  19686  ply1basfvi  19813  coe1tm  19845  ply1coe  19868  zzngim  20102  cnmsgnsubg  20124  psgninv  20129  zrhpsgnmhm  20131  neitr  21192  comppfsc  21543  kgeni  21548  xkoinjcn  21698  ufprim  21920  metreslem  22374  restmetu  22582  retopbas  22771  cnfldms  22786  qdensere2  22807  xrsmopn  22822  metdscn2  22867  pcoass  23030  recvs  23152  zclmncvs  23154  iscmet3lem3  23294  cncms  23357  cnfldcusp  23359  resscdrg  23360  rrxprds  23383  ovoliunnul  23482  uniioombllem4  23561  vitalilem5  23587  mbfres  23619  ismbf3d  23629  i1fima  23653  i1fd  23656  itg2cnlem1  23736  itgss3  23789  ellimc2  23849  limccnp2  23864  cpnres  23908  lhop  23987  plyeq0  24175  plypf1  24176  sinhalfpilem  24424  sincos6thpi  24476  sincos3rdpi  24477  pige3  24478  dfrelog  24520  logimul  24568  logneg2  24569  dvlog  24605  cxpsqrt  24657  ang180lem2  24748  ang180lem3  24749  ang180lem4  24750  quart1  24791  asin1  24829  atan0  24843  atanlogsublem  24850  atan1  24863  log2tlbnd  24880  log2ublem2  24882  log2ub  24884  basellem8  25022  cht2  25106  ppiub  25137  bposlem6  25222  bposlem8  25224  bposlem9  25225  lgsdir2lem3  25260  lgseisenlem1  25308  lgseisenlem2  25309  lgsquadlem1  25313  lgsquadlem2  25314  2lgsoddprmlem2  25342  chebbnd1  25369  istrkg3ld  25568  tgcgr4  25634  motplusg  25645  ax5seglem7  26023  ex-un  27606  ex-sqrt  27636  ipdirilem  28006  ipasslem10  28016  hisubcomi  28283  normlem0  28288  norm3difi  28326  norm3lem  28328  polid2i  28336  chdmj1i  28662  chjjdiri  28705  spansn0  28722  pjoml4i  28768  cmbr3i  28781  qlaxr3i  28817  honpcani  29006  honpncani  29008  lnopunilem1  29191  lnophmlem2  29198  lnfn0i  29223  pjbdlni  29330  pjclem1  29376  pjclem3  29378  pjci  29381  atomli  29563  atabs2i  29583  mddmdin0i  29612  difeq  29674  disjdifprg  29707  imadifxp  29733  fnresin  29751  ofpreima2  29787  df1stres  29802  df2ndres  29803  cnvoprabOLD  29819  dfdec100  29897  decdiv10  29923  dpmul100  29924  dpmul1000  29926  dpexpp1  29935  dpadd2  29937  dpadd  29938  dpmul  29940  dpmul4  29941  threehalves  29942  xrge0base  30004  xrge00  30005  xrge0mulgnn0  30008  xrge0slmod  30163  lmatfvlem  30200  xrge0iifcnv  30298  lmxrge0  30317  cnrrext  30373  qqtopn  30374  esumrnmpt2  30449  esumpfinvallem  30455  unelldsys  30540  ldgenpisyslem1  30545  measunl  30598  mbfmcst  30640  difelcarsg  30691  carsggect  30699  sibfof  30721  eulerpartlemmf  30756  fib2  30783  fib3  30784  fib4  30785  fib5  30786  fib6  30787  0rrv  30832  coinfliprv  30863  ballotlem2  30869  prodfzo03  31000  chtvalz  31026  hgt750lemd  31045  hgt750lem  31048  hgt750lem2  31049  kur14lem6  31510  kur14lem7  31511  cvmlift2lem12  31613  problem5  31879  quad3  31880  divcnvlin  31934  logi  31936  bj-2upln1upl  33316  bj-rest0  33351  relowlssretop  33521  relowlpssretop  33522  1oequni2o  33526  curunc  33698  ptrest  33715  poimirlem16  33732  poimirlem30  33746  mblfinlem2  33754  ovoliunnfl  33758  voliunnfl  33760  itg2addnclem2  33768  ftc1anclem5  33795  ftc1anclem6  33796  sdc  33845  heiborlem3  33917  xrnresex  34471  dvh4dimN  37222  dnnumch1  38109  aomclem6  38124  areaquad  38296  unitadd  38992  seff  39002  sblpnf  39003  hashnzfz  39013  lhe4.4ex1a  39022  xrtgcntopre  40182  iccdifioo  40216  itgsin0pilem1  40639  stoweidlem13  40703  stoweidlem26  40716  fourierdlem62  40858  fourierdlem102  40898  fourierdlem114  40910  fourierswlem  40920  fouriersw  40921  sge0tsms  41070  meaiuninc  41171  fmtno4prmfac  42053  41prothprm  42105  2zrngasgrp  42502  2zrngmsgrp  42509  mvlraddi  43079  mvlrmuli  43088  i2linesi  43089