Theorem eqtr3i 2756

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

Syntax hints:   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  3eqtr3i  2762  3eqtr3ri  2763  rabrabiOLD  3444  unundi  4171  unundir  4172  inindi  4228  inindir  4229  dfin4  4269  difun1  4291  difabs  4295  notab  4306  dif0  4377  disjdifr  4477  difdifdir  4496  pwundif  4631  tpidm13  4765  intmin2  4983  iunxdif3  5103  univ  5457  iunxpconst  5754  rnresi  6084  rnresv  6212  cnvsn0  6221  resdmres  6243  coi2  6274  coires1  6275  dfdm2  6292  isarep2  6650  resasplit  6772  ssimaex  6987  fnreseql  7061  resfunexg  7232  mpompt  7539  caov31  7655  fvresex  7973  xpexgALT  7995  1st2val  8031  2nd2val  8032  cnvoprab  8074  fnsuppeq0  8206  ecopovtrn  8849  limensuci  9191  pssnnOLD  9299  pwfilem  9358  r1sucg  9812  jech9.3  9857  rankbnd2  9912  djuin  9961  compss  10419  zorn2lem4  10542  iunfo  10582  cardf  10593  alephsuc3  10623  fpwwe2lem12  10685  rankcf  10820  halfnq  11019  addclprlem2  11060  mulgt0sr  11148  mul02lem2  11441  mul02  11442  addrid  11444  mvlladdi  11528  mvllmuli  12098  infrenegsup  12249  8th4div3  12484  nneo  12698  nummac  12774  numadd  12776  numaddc  12777  nummul1c  12778  decbin0  12869  rpsup  13886  resup  13887  om2uzrdg  13976  m1expcl2  14105  facnn  14292  fac0  14293  faclbnd4lem1  14310  4bc3eq4  14345  hasheq0  14380  f1oun2prg  14926  sqrt1  15276  sqrt4  15277  sqrt9  15278  rddif  15345  abs3lemi  15415  sumss2  15730  divcnvshft  15859  geo2sum2  15878  geomulcvg  15880  geoihalfsum  15886  risefall0lem  16028  bpoly2  16059  bpoly3  16060  sin0  16151  efival  16154  ef01bndlem  16186  cos2bnd  16190  sin4lt0  16197  flodddiv4  16415  2prm  16693  unbenlem  16910  dec5dvds  17066  modxai  17070  mod2xi  17071  mod2xnegi  17073  gcdi  17075  numexp2x  17081  decsplit  17085  setsid  17210  mreexexlem3d  17659  oppchom  17729  2oppchomf  17739  isoval  17781  estrres  18163  oppchofcl  18285  oyoncl  18295  mvdco  19443  m1expaddsub  19496  psgn0fv0  19509  oppglsm  19640  dprd2da  20042  ring1  20289  opprsubg  20334  lsppratlem1  21128  pzriprnglem7  21477  zzngim  21550  cnmsgnsubg  21573  psgninv  21578  zrhpsgnmhm  21580  ply1basfvi  22230  coe1tm  22264  ply1coe  22289  comppfsc  23527  kgeni  23532  xkoinjcn  23682  ufprim  23904  metreslem  24359  retopbas  24768  cnfldms  24783  qdensere2  24804  xrsmopn  24819  metdscn2  24864  pcoass  25042  recvs  25164  recvsOLD  25165  zclmncvs  25167  iscmet3lem3  25309  cncms  25374  cnfldcusp  25376  resscdrg  25377  rrxprds  25408  ovoliunnul  25527  uniioombllem4  25606  vitalilem5  25632  mbfres  25664  ismbf3d  25674  i1fima  25698  i1fd  25701  itg2cnlem1  25782  itgss3  25835  ellimc2  25897  limccnp2  25912  cpnres  25958  lhop  26040  plyeq0  26238  plypf1  26239  sinhalfpilem  26491  sincos6thpi  26543  sincos3rdpi  26544  pige3ALT  26547  dfrelog  26592  logi  26614  logimul  26641  logneg2  26642  dvlog  26678  cxpsqrt  26730  ang180lem2  26838  ang180lem3  26839  ang180lem4  26840  quart1  26884  asin1  26922  atan0  26936  atanlogsublem  26943  atan1  26956  log2tlbnd  26973  log2ublem2  26975  log2ub  26977  basellem8  27116  cht2  27200  ppiub  27233  bposlem6  27318  bposlem8  27320  bposlem9  27321  lgsdir2lem3  27356  lgseisenlem1  27404  lgseisenlem2  27405  lgsquadlem1  27409  lgsquadlem2  27410  2lgsoddprmlem2  27438  chebbnd1  27501  negsbdaylem  28065  om2noseqrdg  28278  istrkg3ld  28388  tgcgr4  28458  motplusg  28469  ax5seglem7  28869  ex-un  30357  ex-sqrt  30387  ipdirilem  30762  ipasslem10  30772  hisubcomi  31037  normlem0  31042  norm3difi  31080  norm3lem  31082  polid2i  31090  chdmj1i  31414  chjjdiri  31457  spansn0  31474  pjoml4i  31520  cmbr3i  31533  qlaxr3i  31569  honpcani  31758  honpncani  31760  lnopunilem1  31943  lnophmlem2  31950  lnfn0i  31975  pjbdlni  32082  pjclem1  32128  pjclem3  32130  pjci  32133  atomli  32315  atabs2i  32335  mddmdin0i  32364  imadifxp  32521  fnresin  32543  ofpreima2  32583  df1stres  32615  df2ndres  32616  cnvoprabOLD  32634  nn0disj01  32719  dfdec100  32731  decdiv10  32757  dpmul100  32758  dpmul1000  32760  dpexpp1  32769  dpadd2  32771  dpadd  32772  dpmul  32774  dpmul4  32775  threehalves  32776  xrge0base  32894  xrge00  32895  xrge0mulgnn0  32898  cyc2fv1  32999  cyc3conja  33035  xrge0slmod  33223  opprqusplusg  33364  opprqusmulr  33366  lmatfvlem  33630  xrge0iifcnv  33748  lmxrge0  33767  cnrrext  33825  qqtopn  33826  esumrnmpt2  33901  esumpfinvallem  33907  unelldsys  33991  ldgenpisyslem1  33996  measunl  34049  mbfmcst  34093  difelcarsg  34144  carsggect  34152  sibfof  34174  eulerpartlemmf  34209  fib2  34236  fib3  34237  fib4  34238  fib5  34239  fib6  34240  0rrv  34285  coinfliprv  34316  ballotlem2  34322  prodfzo03  34449  chtvalz  34475  hgt750lemd  34494  hgt750lem  34497  hgt750lem2  34498  kur14lem6  35039  kur14lem7  35040  cvmlift2lem12  35142  problem5  35497  quad3  35498  divcnvlin  35555  bj-2upln1upl  36731  bj-rest0  36800  relowlssretop  37070  relowlpssretop  37071  1oequni2o  37075  curunc  37303  ptrest  37320  poimirlem16  37337  poimirlem30  37351  mblfinlem2  37359  ovoliunnfl  37363  voliunnfl  37365  itg2addnclem2  37373  ftc1anclem5  37398  ftc1anclem6  37399  sdc  37445  heiborlem3  37514  xrnresex  38104  dvh4dimN  41146  12gcd5e1  41702  60gcd6e6  41703  60gcd7e1  41704  420gcd8e4  41705  lcmeprodgcdi  41706  lcmineqlem23  41750  sq3deccom12  42103  sn-it1ei  42216  sn-0tie0  42219  sn-inelr  42247  acos1half  42328  dnnumch1  42705  aomclem6  42720  areaquad  42881  naddov4  43049  unitadd  43862  seff  43983  sblpnf  43984  hashnzfz  43994  lhe4.4ex1a  44003  xrtgcntopre  45094  iccdifioo  45133  itgsin0pilem1  45571  stoweidlem13  45634  stoweidlem26  45647  fourierdlem62  45789  fourierdlem102  45829  fourierdlem114  45841  fourierswlem  45851  fouriersw  45852  sge0tsms  46001  meaiuninc  46102  tworepnotupword  46505  fmtno4prmfac  47144  41prothprm  47191  dfclnbgr4  47396  2zrngasgrp  47623  2zrngmsgrp  47630  mvlraddi  48518  mvlrmuli  48525  i2linesi  48526