Theorem eqtr3i 2767

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 2746	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2765	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtr3i  2773  3eqtr3ri  2774  rabrabiOLD  3429  unundi  4125  unundir  4126  inindi  4181  inindir  4182  dfin4  4222  difun1  4244  difabs  4248  notab  4259  dif0  4327  disjdifr  4427  difdifdir  4444  pwundif  4579  tpidm13  4712  intmin2  4931  iunxdif3  5050  univ  5403  iunxpconst  5697  rnresi  6020  rnresv  6146  cnvsn0  6155  resdmres  6177  coi2  6208  coires1  6209  dfdm2  6226  isarep2  6584  resasplit  6704  ssimaex  6918  fnreseql  6990  resfunexg  7156  mpompt  7459  caov31  7572  fvresex  7879  xpexgALT  7901  1st2val  7936  2nd2val  7937  cnvoprab  7977  fnsuppeq0  8087  ecopovtrn  8689  limensuci  9027  pwfilem  9051  pssnnOLD  9139  r1sucg  9635  jech9.3  9680  rankbnd2  9735  djuin  9784  compss  10242  zorn2lem4  10365  iunfo  10405  cardf  10416  alephsuc3  10446  fpwwe2lem12  10508  rankcf  10643  halfnq  10842  addclprlem2  10883  mulgt0sr  10971  mul02lem2  11262  mul02  11263  addid1  11265  mvlladdi  11349  mvllmuli  11918  infrenegsup  12068  8th4div3  12303  nneo  12514  nummac  12592  numadd  12594  numaddc  12595  nummul1c  12596  decbin0  12687  rpsup  13696  resup  13697  om2uzrdg  13786  m1expcl2  13914  facnn  14099  fac0  14100  faclbnd4lem1  14117  4bc3eq4  14152  hasheq0  14187  f1oun2prg  14734  sqrt1  15087  sqrt4  15088  sqrt9  15089  rddif  15156  abs3lemi  15226  sumss2  15542  divcnvshft  15671  geo2sum2  15690  geomulcvg  15692  geoihalfsum  15698  risefall0lem  15840  bpoly2  15871  bpoly3  15872  sin0  15962  efival  15965  ef01bndlem  15997  cos2bnd  16001  sin4lt0  16008  flodddiv4  16226  2prm  16499  unbenlem  16711  dec5dvds  16867  modxai  16871  mod2xi  16872  mod2xnegi  16874  gcdi  16876  numexp2x  16882  decsplit  16886  setsid  17011  mreexexlem3d  17457  oppchom  17527  2oppchomf  17537  isoval  17579  estrres  17958  oppchofcl  18080  oyoncl  18090  mvdco  19154  m1expaddsub  19207  psgn0fv0  19220  oppglsm  19348  dprd2da  19744  ring1  19940  opprsubg  19977  lsppratlem1  20519  zzngim  20870  cnmsgnsubg  20892  psgninv  20897  zrhpsgnmhm  20899  ply1basfvi  21522  coe1tm  21554  ply1coe  21577  comppfsc  22793  kgeni  22798  xkoinjcn  22948  ufprim  23170  metreslem  23625  retopbas  24034  cnfldms  24049  qdensere2  24070  xrsmopn  24085  metdscn2  24130  pcoass  24297  recvs  24419  recvsOLD  24420  zclmncvs  24422  iscmet3lem3  24564  cncms  24629  cnfldcusp  24631  resscdrg  24632  rrxprds  24663  ovoliunnul  24781  uniioombllem4  24860  vitalilem5  24886  mbfres  24918  ismbf3d  24928  i1fima  24952  i1fd  24955  itg2cnlem1  25036  itgss3  25089  ellimc2  25151  limccnp2  25166  cpnres  25211  lhop  25290  plyeq0  25482  plypf1  25483  sinhalfpilem  25730  sincos6thpi  25782  sincos3rdpi  25783  pige3ALT  25786  dfrelog  25831  logimul  25879  logneg2  25880  dvlog  25916  cxpsqrt  25968  ang180lem2  26070  ang180lem3  26071  ang180lem4  26072  quart1  26116  asin1  26154  atan0  26168  atanlogsublem  26175  atan1  26188  log2tlbnd  26205  log2ublem2  26207  log2ub  26209  basellem8  26347  cht2  26431  ppiub  26462  bposlem6  26547  bposlem8  26549  bposlem9  26550  lgsdir2lem3  26585  lgseisenlem1  26633  lgseisenlem2  26634  lgsquadlem1  26638  lgsquadlem2  26639  2lgsoddprmlem2  26667  chebbnd1  26730  istrkg3ld  27177  tgcgr4  27247  motplusg  27258  ax5seglem7  27658  ex-un  29142  ex-sqrt  29172  ipdirilem  29545  ipasslem10  29555  hisubcomi  29820  normlem0  29825  norm3difi  29863  norm3lem  29865  polid2i  29873  chdmj1i  30197  chjjdiri  30240  spansn0  30257  pjoml4i  30303  cmbr3i  30316  qlaxr3i  30352  honpcani  30541  honpncani  30543  lnopunilem1  30726  lnophmlem2  30733  lnfn0i  30758  pjbdlni  30865  pjclem1  30911  pjclem3  30913  pjci  30916  atomli  31098  atabs2i  31118  mddmdin0i  31147  imadifxp  31291  fnresin  31312  ofpreima2  31354  df1stres  31387  df2ndres  31388  cnvoprabOLD  31406  dfdec100  31495  decdiv10  31521  dpmul100  31522  dpmul1000  31524  dpexpp1  31533  dpadd2  31535  dpadd  31536  dpmul  31538  dpmul4  31539  threehalves  31540  xrge0base  31645  xrge00  31646  xrge0mulgnn0  31649  cyc2fv1  31739  cyc3conja  31775  xrge0slmod  31908  lmatfvlem  32127  xrge0iifcnv  32245  lmxrge0  32264  cnrrext  32322  qqtopn  32323  esumrnmpt2  32398  esumpfinvallem  32404  unelldsys  32488  ldgenpisyslem1  32493  measunl  32546  mbfmcst  32590  difelcarsg  32641  carsggect  32649  sibfof  32671  eulerpartlemmf  32706  fib2  32733  fib3  32734  fib4  32735  fib5  32736  fib6  32737  0rrv  32782  coinfliprv  32813  ballotlem2  32819  prodfzo03  32947  chtvalz  32973  hgt750lemd  32992  hgt750lem  32995  hgt750lem2  32996  kur14lem6  33536  kur14lem7  33537  cvmlift2lem12  33639  problem5  33990  quad3  33991  divcnvlin  34053  logi  34055  bj-2upln1upl  35351  bj-rest0  35420  relowlssretop  35690  relowlpssretop  35691  1oequni2o  35695  curunc  35915  ptrest  35932  poimirlem16  35949  poimirlem30  35963  mblfinlem2  35971  ovoliunnfl  35975  voliunnfl  35977  itg2addnclem2  35985  ftc1anclem5  36010  ftc1anclem6  36011  sdc  36058  heiborlem3  36127  xrnresex  36724  dvh4dimN  39766  12gcd5e1  40316  60gcd6e6  40317  60gcd7e1  40318  420gcd8e4  40319  lcmeprodgcdi  40320  lcmineqlem23  40364  acos1half  40478  sq3deccom12  40629  it1ei  40729  sn-0tie0  40732  sn-inelr  40746  dnnumch1  41183  aomclem6  41198  areaquad  41362  unitadd  42179  seff  42300  sblpnf  42301  hashnzfz  42311  lhe4.4ex1a  42320  xrtgcntopre  43406  iccdifioo  43441  itgsin0pilem1  43879  stoweidlem13  43942  stoweidlem26  43955  fourierdlem62  44097  fourierdlem102  44137  fourierdlem114  44149  fourierswlem  44159  fouriersw  44160  sge0tsms  44307  meaiuninc  44408  tworepnotupword  44803  fmtno4prmfac  45442  41prothprm  45489  2zrngasgrp  45916  2zrngmsgrp  45923  mvlraddi  46891  mvlrmuli  46898  i2linesi  46899