Theorem eqtr3i 2763

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  3eqtr3i  2769  3eqtr3ri  2770  rabrabiOLD  3457  unundi  4171  unundir  4172  inindi  4227  inindir  4228  dfin4  4268  difun1  4290  difabs  4294  notab  4305  dif0  4373  disjdifr  4473  difdifdir  4492  pwundif  4627  tpidm13  4761  intmin2  4980  iunxdif3  5099  univ  5452  iunxpconst  5749  rnresi  6075  rnresv  6201  cnvsn0  6210  resdmres  6232  coi2  6263  coires1  6264  dfdm2  6281  isarep2  6640  resasplit  6762  ssimaex  6977  fnreseql  7050  resfunexg  7217  mpompt  7522  caov31  7636  fvresex  7946  xpexgALT  7968  1st2val  8003  2nd2val  8004  cnvoprab  8046  fnsuppeq0  8177  ecopovtrn  8814  limensuci  9153  pwfilem  9177  pssnnOLD  9265  r1sucg  9764  jech9.3  9809  rankbnd2  9864  djuin  9913  compss  10371  zorn2lem4  10494  iunfo  10534  cardf  10545  alephsuc3  10575  fpwwe2lem12  10637  rankcf  10772  halfnq  10971  addclprlem2  11012  mulgt0sr  11100  mul02lem2  11391  mul02  11392  addrid  11394  mvlladdi  11478  mvllmuli  12047  infrenegsup  12197  8th4div3  12432  nneo  12646  nummac  12722  numadd  12724  numaddc  12725  nummul1c  12726  decbin0  12817  rpsup  13831  resup  13832  om2uzrdg  13921  m1expcl2  14051  facnn  14235  fac0  14236  faclbnd4lem1  14253  4bc3eq4  14288  hasheq0  14323  f1oun2prg  14868  sqrt1  15218  sqrt4  15219  sqrt9  15220  rddif  15287  abs3lemi  15357  sumss2  15672  divcnvshft  15801  geo2sum2  15820  geomulcvg  15822  geoihalfsum  15828  risefall0lem  15970  bpoly2  16001  bpoly3  16002  sin0  16092  efival  16095  ef01bndlem  16127  cos2bnd  16131  sin4lt0  16138  flodddiv4  16356  2prm  16629  unbenlem  16841  dec5dvds  16997  modxai  17001  mod2xi  17002  mod2xnegi  17004  gcdi  17006  numexp2x  17012  decsplit  17016  setsid  17141  mreexexlem3d  17590  oppchom  17660  2oppchomf  17670  isoval  17712  estrres  18091  oppchofcl  18213  oyoncl  18223  mvdco  19313  m1expaddsub  19366  psgn0fv0  19379  oppglsm  19510  dprd2da  19912  ring1  20122  opprsubg  20166  lsppratlem1  20760  zzngim  21108  cnmsgnsubg  21130  psgninv  21135  zrhpsgnmhm  21137  ply1basfvi  21763  coe1tm  21795  ply1coe  21820  comppfsc  23036  kgeni  23041  xkoinjcn  23191  ufprim  23413  metreslem  23868  retopbas  24277  cnfldms  24292  qdensere2  24313  xrsmopn  24328  metdscn2  24373  pcoass  24540  recvs  24662  recvsOLD  24663  zclmncvs  24665  iscmet3lem3  24807  cncms  24872  cnfldcusp  24874  resscdrg  24875  rrxprds  24906  ovoliunnul  25024  uniioombllem4  25103  vitalilem5  25129  mbfres  25161  ismbf3d  25171  i1fima  25195  i1fd  25198  itg2cnlem1  25279  itgss3  25332  ellimc2  25394  limccnp2  25409  cpnres  25454  lhop  25533  plyeq0  25725  plypf1  25726  sinhalfpilem  25973  sincos6thpi  26025  sincos3rdpi  26026  pige3ALT  26029  dfrelog  26074  logimul  26122  logneg2  26123  dvlog  26159  cxpsqrt  26211  ang180lem2  26315  ang180lem3  26316  ang180lem4  26317  quart1  26361  asin1  26399  atan0  26413  atanlogsublem  26420  atan1  26433  log2tlbnd  26450  log2ublem2  26452  log2ub  26454  basellem8  26592  cht2  26676  ppiub  26707  bposlem6  26792  bposlem8  26794  bposlem9  26795  lgsdir2lem3  26830  lgseisenlem1  26878  lgseisenlem2  26879  lgsquadlem1  26883  lgsquadlem2  26884  2lgsoddprmlem2  26912  chebbnd1  26975  negsbdaylem  27530  istrkg3ld  27712  tgcgr4  27782  motplusg  27793  ax5seglem7  28193  ex-un  29677  ex-sqrt  29707  ipdirilem  30082  ipasslem10  30092  hisubcomi  30357  normlem0  30362  norm3difi  30400  norm3lem  30402  polid2i  30410  chdmj1i  30734  chjjdiri  30777  spansn0  30794  pjoml4i  30840  cmbr3i  30853  qlaxr3i  30889  honpcani  31078  honpncani  31080  lnopunilem1  31263  lnophmlem2  31270  lnfn0i  31295  pjbdlni  31402  pjclem1  31448  pjclem3  31450  pjci  31453  atomli  31635  atabs2i  31655  mddmdin0i  31684  imadifxp  31832  fnresin  31850  ofpreima2  31891  df1stres  31925  df2ndres  31926  cnvoprabOLD  31945  dfdec100  32036  decdiv10  32062  dpmul100  32063  dpmul1000  32065  dpexpp1  32074  dpadd2  32076  dpadd  32077  dpmul  32079  dpmul4  32080  threehalves  32081  xrge0base  32186  xrge00  32187  xrge0mulgnn0  32190  cyc2fv1  32280  cyc3conja  32316  xrge0slmod  32463  opprqusplusg  32603  opprqusmulr  32605  lmatfvlem  32795  xrge0iifcnv  32913  lmxrge0  32932  cnrrext  32990  qqtopn  32991  esumrnmpt2  33066  esumpfinvallem  33072  unelldsys  33156  ldgenpisyslem1  33161  measunl  33214  mbfmcst  33258  difelcarsg  33309  carsggect  33317  sibfof  33339  eulerpartlemmf  33374  fib2  33401  fib3  33402  fib4  33403  fib5  33404  fib6  33405  0rrv  33450  coinfliprv  33481  ballotlem2  33487  prodfzo03  33615  chtvalz  33641  hgt750lemd  33660  hgt750lem  33663  hgt750lem2  33664  kur14lem6  34202  kur14lem7  34203  cvmlift2lem12  34305  problem5  34654  quad3  34655  divcnvlin  34702  logi  34704  bj-2upln1upl  35905  bj-rest0  35974  relowlssretop  36244  relowlpssretop  36245  1oequni2o  36249  curunc  36470  ptrest  36487  poimirlem16  36504  poimirlem30  36518  mblfinlem2  36526  ovoliunnfl  36530  voliunnfl  36532  itg2addnclem2  36540  ftc1anclem5  36565  ftc1anclem6  36566  sdc  36612  heiborlem3  36681  xrnresex  37276  dvh4dimN  40318  12gcd5e1  40868  60gcd6e6  40869  60gcd7e1  40870  420gcd8e4  40871  lcmeprodgcdi  40872  lcmineqlem23  40916  sq3deccom12  41202  it1ei  41309  sn-0tie0  41312  sn-inelr  41338  acos1half  41415  dnnumch1  41786  aomclem6  41801  areaquad  41965  naddov4  42133  unitadd  42947  seff  43068  sblpnf  43069  hashnzfz  43079  lhe4.4ex1a  43088  xrtgcntopre  44189  iccdifioo  44228  itgsin0pilem1  44666  stoweidlem13  44729  stoweidlem26  44742  fourierdlem62  44884  fourierdlem102  44924  fourierdlem114  44936  fourierswlem  44946  fouriersw  44947  sge0tsms  45096  meaiuninc  45197  tworepnotupword  45600  fmtno4prmfac  46240  41prothprm  46287  pzriprnglem7  46811  2zrngasgrp  46838  2zrngmsgrp  46845  mvlraddi  47817  mvlrmuli  47824  i2linesi  47825