Theorem eqtr3i 2790

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  3eqtr3i  2796  3eqtr3ri  2797  unundi  4129  unundir  4130  inindi  4187  inindir  4188  dfin4  4231  difun1  4252  difabs  4256  notab  4267  dif0  4334  difdifdir  4454  pwundif  4589  tpidm13  4724  intmin2  4942  iunxdif3  5063  univ  5434  iunxpconst  5736  resdmdfsn  6033  rnresi  6079  rnresv  6202  imadifssran  6204  cnvsn0  6213  resdmres  6235  coi2  6267  coires1  6268  dfdm2  6286  isarep2  6629  resasplit  6752  ssimaex  6970  fnreseql  7047  resfunexg  7220  mpompt  7533  caov31  7649  fvresex  7963  xpexgALT  7984  1st2val  8020  2nd2val  8021  cnvoprab  8063  fnsuppeq0  8194  ecopovtrn  8824  limensuci  9148  pwfilem  9284  r1sucg  9748  jech9.3  9793  rankbnd2  9848  djuin  9920  compss  10375  zorn2lem4  10498  iunfo  10538  cardf  10549  alephsuc3  10580  fpwwe2lem12  10642  rankcf  10777  halfnq  10976  addclprlem2  11017  mulgt0sr  11105  mul02lem2  11402  mul02  11403  addrid  11405  mvlladdi  11491  mvllmuli  12063  infrenegsup  12213  halfpm6th  12481  nneo  12696  nummac  12777  numadd  12779  numaddc  12780  nummul1c  12781  decbin0  12874  fz00m1  13590  rpsup  13917  resup  13918  om2uzrdg  14010  m1expcl2  14139  facnn  14329  fac0  14330  faclbnd4lem1  14347  4bc3eq4  14382  hasheq0  14417  f1oun2prg  14978  sqrt1  15346  sqrt4  15347  sqrt9  15348  rddif  15416  abs3lemi  15486  sumss2  15800  divcnvshft  15932  geo2sum2  15951  geomulcvg  15953  geoihalfsum  15959  bpoly2  16133  bpoly3  16134  sin0  16227  efival  16230  ef01bndlem  16262  cos2bnd  16266  sin4lt0  16273  flodddiv4  16495  2prm  16772  unbenlem  16990  dec5dvds  17146  modxai  17150  mod2xi  17151  mod2xnegi  17153  gcdi  17155  numexp2x  17160  decsplit  17164  setsid  17289  xrge0base  17683  mreexexlem3d  17724  oppchom  17793  2oppchomf  17802  isoval  17844  estrres  18217  oppchofcl  18338  oyoncl  18348  mvdco  19559  m1expaddsub  19612  psgn0fv0  19625  oppglsm  19756  dprd2da  20158  ring1  20439  opprsubg  20480  lsppratlem1  21321  pzriprnglem7  21687  zzngim  21752  cnmsgnsubg  21777  psgninv  21782  zrhpsgnmhm  21784  ply1basfvi  22450  coe1tm  22484  ply1coe  22508  comppfsc  23740  kgeni  23745  xkoinjcn  23895  ufprim  24117  metreslem  24570  retopbas  24968  cnfldms  24983  qdensere2  25005  xrsmopn  25021  metdscn2  25066  pcoass  25234  recvs  25356  zclmncvs  25358  iscmet3lem3  25500  cncms  25565  cnfldcusp  25567  resscdrg  25568  rrxprds  25599  ovoliunnul  25717  uniioombllem4  25796  vitalilem5  25822  mbfres  25854  ismbf3d  25864  i1fima  25888  i1fd  25891  itg2cnlem1  25971  itgss3  26025  ellimc2  26087  limccnp2  26102  cpnres  26147  lhop  26226  plyeq0  26419  plypf1  26420  sinhalfpilem  26679  sincos6thpi  26732  sincos3rdpi  26733  pige3ALT  26736  dfrelog  26781  logi  26803  logimul  26830  logneg2  26831  dvlog  26867  cxpsqrt  26919  ang180lem2  27026  ang180lem3  27027  ang180lem4  27028  quart1  27072  asin1  27110  atan0  27124  atanlogsublem  27131  atan1  27144  log2tlbnd  27161  log2ublem2  27163  log2ub  27165  cht2  27387  ppiub  27419  bposlem6  27504  bposlem8  27506  bposlem9  27507  lgsdir2lem3  27542  lgseisenlem1  27590  lgseisenlem2  27591  lgsquadlem1  27595  lgsquadlem2  27596  2lgsoddprmlem2  27624  chebbnd1  27687  negbdaylem  28300  om2noseqrdg  28548  zseo  28666  bdaypw2n0bndlem  28707  istrkg3ld  28781  tgcgr4  28851  motplusg  28862  ax5seglem7  29340  ex-un  30846  ex-sqrt  30876  ipdirilem  31252  ipasslem10  31262  hisubcomi  31527  normlem0  31532  norm3difi  31570  norm3lem  31572  polid2i  31580  chdmj1i  31904  chjjdiri  31947  spansn0  31964  pjoml4i  32010  cmbr3i  32023  qlaxr3i  32059  honpcani  32248  honpncani  32250  lnopunilem1  32433  lnophmlem2  32440  lnfn0i  32465  pjbdlni  32572  pjclem1  32618  pjclem3  32620  pjci  32623  atomli  32805  atabs2i  32825  mddmdin0i  32854  imadifxp  33017  fnresin  33040  ofpreima2  33082  df1stres  33120  df2ndres  33121  nn0disj01  33233  dfdec100  33244  decdiv10  33285  dpmul100  33286  dpmul1000  33288  dpexpp1  33297  dpadd2  33299  dpadd  33300  dpmul  33302  dpmul4  33303  threehalves  33304  xrge00  33398  xrge0mulgnn0  33399  cyc2fv1  33505  cyc3conja  33541  elrgspnlem4  33629  xrge0slmod  33732  opprqusplusg  33835  opprqusmulr  33837  selvply1rhmlemb  33973  extvfvcl  33990  2sqr3nconstr  34235  cos9thpiminplylem1  34236  cos9thpiminplylem5  34240  cos9thpinconstrlem2  34244  lmatfvlem  34269  xrge0iifcnv  34387  lmxrge0  34406  cnrrext  34464  qqtopn  34465  esumrnmpt2  34522  esumpfinvallem  34528  unelldsys  34613  ldgenpisyslem1  34618  measunl  34671  mbfmcst  34714  difelcarsg  34765  carsggect  34773  sibfof  34795  eulerpartlemmf  34830  fib2  34857  fib3  34858  fib4  34859  fib5  34860  fib6  34861  0rrv  34906  coinfliprv  34938  ballotlem2  34944  prodfzo03  35055  chtvalz  35081  hgt750lemd  35100  hgt750lem  35103  hgt750lem2  35104  1enumen  35543  kur14lem6  35740  kur14lem7  35741  cvmlift2lem12  35843  problem5  36198  quad3  36199  divcnvlin  36262  in-ax8  36793  bj-2upln1upl  37717  bj-rest0  37792  relowlssretop  38066  relowlpssretop  38067  1oequni2o  38071  curunc  38310  ptrest  38327  poimirlem16  38344  poimirlem30  38358  mblfinlem2  38366  ovoliunnfl  38370  voliunnfl  38372  itg2addnclem2  38380  ftc1anclem5  38405  ftc1anclem6  38406  sdc  38453  heiborlem3  38522  xrnresex  39136  dmxrncnvepres  39139  dvh4dimN  42279  12gcd5e1  42828  60gcd6e6  42829  60gcd7e1  42830  420gcd8e4  42831  lcmeprodgcdi  42832  25or6to4  43031  sq3deccom12  43109  asin1half  43176  acos1half  43177  redvmptabs  43179  readvrec  43181  sn-it1ei  43256  sn-0tie0  43283  dnnumch1  43829  aomclem6  43844  areaquad  44001  naddov4  44168  unitadd  44979  seff  45077  sblpnf  45078  hashnzfz  45088  lhe4.4ex1a  45097  xrtgcntopre  46250  iccdifioo  46289  itgsin0pilem1  46722  stoweidlem13  46785  stoweidlem26  46798  fourierdlem62  46940  fourierdlem102  46980  fourierdlem114  46992  fourierswlem  47002  fouriersw  47003  sge0tsms  47152  meaiuninc  47253  cos5t  47674  fmtno4prmfac  48382  41prothprm  48429  ppivalnn4  48437  dfclnbgr4  48647  2zrngasgrp  49068  2zrngmsgrp  49075  tposres3  49716  eloppf  49968  setc1onsubc  50437  mvlraddi  50606  mvlrmuli  50612  i2linesi  50613