Theorem eqtr3i 2754

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716

This theorem is referenced by:  3eqtr3i  2760  3eqtr3ri  2761  rabrabiOLD  3448  unundi  4162  unundir  4163  inindi  4218  inindir  4219  dfin4  4259  difun1  4281  difabs  4285  notab  4296  dif0  4364  disjdifr  4464  difdifdir  4483  pwundif  4618  tpidm13  4752  intmin2  4969  iunxdif3  5088  univ  5441  iunxpconst  5738  rnresi  6064  rnresv  6190  cnvsn0  6199  resdmres  6221  coi2  6252  coires1  6253  dfdm2  6270  isarep2  6629  resasplit  6751  ssimaex  6966  fnreseql  7039  resfunexg  7208  mpompt  7514  caov31  7629  fvresex  7939  xpexgALT  7961  1st2val  7996  2nd2val  7997  cnvoprab  8039  fnsuppeq0  8171  ecopovtrn  8810  limensuci  9149  pwfilem  9173  pssnnOLD  9261  r1sucg  9760  jech9.3  9805  rankbnd2  9860  djuin  9909  compss  10367  zorn2lem4  10490  iunfo  10530  cardf  10541  alephsuc3  10571  fpwwe2lem12  10633  rankcf  10768  halfnq  10967  addclprlem2  11008  mulgt0sr  11096  mul02lem2  11388  mul02  11389  addrid  11391  mvlladdi  11475  mvllmuli  12044  infrenegsup  12194  8th4div3  12429  nneo  12643  nummac  12719  numadd  12721  numaddc  12722  nummul1c  12723  decbin0  12814  rpsup  13828  resup  13829  om2uzrdg  13918  m1expcl2  14048  facnn  14232  fac0  14233  faclbnd4lem1  14250  4bc3eq4  14285  hasheq0  14320  f1oun2prg  14865  sqrt1  15215  sqrt4  15216  sqrt9  15217  rddif  15284  abs3lemi  15354  sumss2  15669  divcnvshft  15798  geo2sum2  15817  geomulcvg  15819  geoihalfsum  15825  risefall0lem  15967  bpoly2  15998  bpoly3  15999  sin0  16089  efival  16092  ef01bndlem  16124  cos2bnd  16128  sin4lt0  16135  flodddiv4  16353  2prm  16626  unbenlem  16840  dec5dvds  16996  modxai  17000  mod2xi  17001  mod2xnegi  17003  gcdi  17005  numexp2x  17011  decsplit  17015  setsid  17140  mreexexlem3d  17589  oppchom  17659  2oppchomf  17669  isoval  17711  estrres  18093  oppchofcl  18215  oyoncl  18225  mvdco  19355  m1expaddsub  19408  psgn0fv0  19421  oppglsm  19552  dprd2da  19954  ring1  20199  opprsubg  20244  lsppratlem1  20988  pzriprnglem7  21342  zzngim  21415  cnmsgnsubg  21438  psgninv  21443  zrhpsgnmhm  21445  ply1basfvi  22082  coe1tm  22114  ply1coe  22139  comppfsc  23358  kgeni  23363  xkoinjcn  23513  ufprim  23735  metreslem  24190  retopbas  24599  cnfldms  24614  qdensere2  24635  xrsmopn  24650  metdscn2  24695  pcoass  24873  recvs  24995  recvsOLD  24996  zclmncvs  24998  iscmet3lem3  25140  cncms  25205  cnfldcusp  25207  resscdrg  25208  rrxprds  25239  ovoliunnul  25358  uniioombllem4  25437  vitalilem5  25463  mbfres  25495  ismbf3d  25505  i1fima  25529  i1fd  25532  itg2cnlem1  25613  itgss3  25666  ellimc2  25728  limccnp2  25743  cpnres  25789  lhop  25871  plyeq0  26065  plypf1  26066  sinhalfpilem  26315  sincos6thpi  26367  sincos3rdpi  26368  pige3ALT  26371  dfrelog  26416  logimul  26464  logneg2  26465  dvlog  26501  cxpsqrt  26553  ang180lem2  26658  ang180lem3  26659  ang180lem4  26660  quart1  26704  asin1  26742  atan0  26756  atanlogsublem  26763  atan1  26776  log2tlbnd  26793  log2ublem2  26795  log2ub  26797  basellem8  26936  cht2  27020  ppiub  27053  bposlem6  27138  bposlem8  27140  bposlem9  27141  lgsdir2lem3  27176  lgseisenlem1  27224  lgseisenlem2  27225  lgsquadlem1  27229  lgsquadlem2  27230  2lgsoddprmlem2  27258  chebbnd1  27321  negsbdaylem  27884  om2noseqrdg  28093  istrkg3ld  28181  tgcgr4  28251  motplusg  28262  ax5seglem7  28662  ex-un  30146  ex-sqrt  30176  ipdirilem  30551  ipasslem10  30561  hisubcomi  30826  normlem0  30831  norm3difi  30869  norm3lem  30871  polid2i  30879  chdmj1i  31203  chjjdiri  31246  spansn0  31263  pjoml4i  31309  cmbr3i  31322  qlaxr3i  31358  honpcani  31547  honpncani  31549  lnopunilem1  31732  lnophmlem2  31739  lnfn0i  31764  pjbdlni  31871  pjclem1  31917  pjclem3  31919  pjci  31922  atomli  32104  atabs2i  32124  mddmdin0i  32153  imadifxp  32301  fnresin  32319  ofpreima2  32360  df1stres  32394  df2ndres  32395  cnvoprabOLD  32414  dfdec100  32503  decdiv10  32529  dpmul100  32530  dpmul1000  32532  dpexpp1  32541  dpadd2  32543  dpadd  32544  dpmul  32546  dpmul4  32547  threehalves  32548  xrge0base  32651  xrge00  32652  xrge0mulgnn0  32655  cyc2fv1  32748  cyc3conja  32784  xrge0slmod  32929  opprqusplusg  33072  opprqusmulr  33074  lmatfvlem  33284  xrge0iifcnv  33402  lmxrge0  33421  cnrrext  33479  qqtopn  33480  esumrnmpt2  33555  esumpfinvallem  33561  unelldsys  33645  ldgenpisyslem1  33650  measunl  33703  mbfmcst  33747  difelcarsg  33798  carsggect  33806  sibfof  33828  eulerpartlemmf  33863  fib2  33890  fib3  33891  fib4  33892  fib5  33893  fib6  33894  0rrv  33939  coinfliprv  33970  ballotlem2  33976  prodfzo03  34104  chtvalz  34130  hgt750lemd  34149  hgt750lem  34152  hgt750lem2  34153  kur14lem6  34691  kur14lem7  34692  cvmlift2lem12  34794  problem5  35143  quad3  35144  divcnvlin  35197  logi  35199  bj-2upln1upl  36395  bj-rest0  36464  relowlssretop  36734  relowlpssretop  36735  1oequni2o  36739  curunc  36960  ptrest  36977  poimirlem16  36994  poimirlem30  37008  mblfinlem2  37016  ovoliunnfl  37020  voliunnfl  37022  itg2addnclem2  37030  ftc1anclem5  37055  ftc1anclem6  37056  sdc  37102  heiborlem3  37171  xrnresex  37766  dvh4dimN  40808  12gcd5e1  41361  60gcd6e6  41362  60gcd7e1  41363  420gcd8e4  41364  lcmeprodgcdi  41365  lcmineqlem23  41409  sq3deccom12  41691  it1ei  41798  sn-0tie0  41801  sn-inelr  41827  acos1half  41904  dnnumch1  42275  aomclem6  42290  areaquad  42454  naddov4  42622  unitadd  43436  seff  43557  sblpnf  43558  hashnzfz  43568  lhe4.4ex1a  43577  xrtgcntopre  44674  iccdifioo  44713  itgsin0pilem1  45151  stoweidlem13  45214  stoweidlem26  45227  fourierdlem62  45369  fourierdlem102  45409  fourierdlem114  45421  fourierswlem  45431  fouriersw  45432  sge0tsms  45581  meaiuninc  45682  tworepnotupword  46085  fmtno4prmfac  46725  41prothprm  46772  2zrngasgrp  47109  2zrngmsgrp  47116  mvlraddi  48005  mvlrmuli  48012  i2linesi  48013