Theorem eqtr3i 2786

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 2770	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2784	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 2155  ax-ext 2733

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

This theorem is used by:  3eqtr3i  2792  3eqtr3ri  2793  unundi  4122  unundir  4123  inindi  4180  inindir  4181  dfin4  4224  difun1  4245  difabs  4249  notab  4260  dif0  4327  difdifdir  4447  pwundif  4582  tpidm13  4717  intmin2  4935  iunxdif3  5055  univ  5419  iunxpconst  5724  resdmdfsn  6021  rnresi  6073  rnresv  6194  imadifssranOLD  6201  cnvsn0  6210  resdmres  6232  coi2  6264  coires1  6265  dfdm2  6283  isarep2  6627  resasplit  6750  ssimaex  6968  fnreseql  7045  resfunexg  7219  mpompt  7532  caov31  7648  fvresex  7970  xpexgALT  7991  1st2val  8027  2nd2val  8028  cnvoprab  8069  fnsuppeq0  8202  ecopovtrn  8834  limensuci  9165  pwfilem  9302  r1sucg  9769  jech9.3OLD  9816  rankbnd2  9879  djuin  9992  compss  10447  zorn2lem4  10570  iunfo  10616  cardf  10627  alephsuc3  10658  fpwwe2lem12  10720  rankcf  10855  halfnq  11054  addclprlem2  11095  mulgt0sr  11183  mul02lem2  11480  mul02  11481  addrid  11483  mvlladdi  11569  mvllmuli  12143  infrenegsup  12293  halfpm6th  12561  nneo  12776  nummac  12857  numadd  12859  numaddc  12860  nummul1c  12861  decbin0  12954  fz00m1  13672  rpsup  13999  resup  14000  om2uzrdg  14092  m1expcl2  14221  facnn  14412  fac0  14413  faclbnd4lem1  14430  4bc3eq4  14465  hasheq0  14500  f1oun2prg  15061  sqrt1  15431  sqrt4  15432  sqrt9  15433  rddif  15501  abs3lemi  15571  sumss2  15885  divcnvshft  16017  geo2sum2  16036  geomulcvg  16038  geoihalfsum  16044  bpoly2  16216  bpoly3  16217  sin0  16310  efival  16313  ef01bndlem  16345  cos2bnd  16349  sin4lt0  16356  flodddiv4  16578  2prm  16860  unbenlem  17079  dec5dvds  17235  modxai  17239  mod2xi  17240  mod2xnegi  17242  gcdi  17244  numexp2x  17249  decsplit  17253  setsid  17378  xrge0base  17772  mreexexlem3d  17813  oppchom  17882  2oppchomf  17891  isoval  17933  estrres  18306  oppchofcl  18427  oyoncl  18437  mvdco  19652  m1expaddsub  19705  psgn0fv0  19718  oppglsm  19849  dprd2da  20251  ring1  20534  opprsubg  20575  lsppratlem1  21418  pzriprnglem7  21786  zzngim  21851  cnmsgnsubg  21876  psgninv  21881  zrhpsgnmhm  21883  ply1basfvi  22551  coe1tm  22585  ply1coe  22609  comppfsc  23844  kgeni  23849  xkoinjcn  23999  ufprim  24221  metreslem  24674  retopbas  25072  cnfldms  25087  qdensere2  25109  xrsmopn  25125  metdscn2  25170  pcoass  25338  recvs  25460  zclmncvs  25462  iscmet3lem3  25604  cncms  25669  cnfldcusp  25671  resscdrg  25672  rrxprds  25703  ovoliunnul  25821  uniioombllem4  25900  vitalilem5  25926  mbfres  25958  ismbf3d  25968  i1fima  25992  i1fd  25995  itg2cnlem1  26075  itgss3  26128  ellimc2  26190  limccnp2  26205  cpnres  26250  lhop  26329  plyeq0  26523  plypf1  26524  sinhalfpilem  26785  sincos6thpi  26837  sincos3rdpi  26838  pige3ALT  26841  dfrelog  26886  logi  26908  logimul  26935  logneg2  26936  dvlog  26972  cxpsqrt  27024  ang180lem2  27131  ang180lem3  27132  ang180lem4  27133  quart1  27177  asin1  27215  atan0  27229  atanlogsublem  27236  atan1  27249  log2tlbnd  27266  log2ublem2  27268  log2ub  27270  cht2  27492  ppiub  27524  bposlem6  27609  bposlem8  27611  bposlem9  27612  lgsdir2lem3  27647  lgseisenlem1  27695  lgseisenlem2  27696  lgsquadlem1  27700  lgsquadlem2  27701  2lgsoddprmlem2  27729  chebbnd1  27792  negbdaylem  28435  om2noseqrdg  28683  zseo  28801  bdaypw2n0bndlem  28842  istrkg3ld  28916  tgcgr4  28987  motplusg  28998  ax5seglem7  29506  ex-un  31018  ex-sqrt  31048  ipdirilem  31424  ipasslem10  31434  hisubcomi  31699  normlem0  31704  norm3difi  31742  norm3lem  31744  polid2i  31752  chdmj1i  32076  chjjdiri  32119  spansn0  32136  pjoml4i  32182  cmbr3i  32195  qlaxr3i  32231  honpcani  32420  honpncani  32422  lnopunilem1  32605  lnophmlem2  32612  lnfn0i  32637  pjbdlni  32744  pjclem1  32790  pjclem3  32792  pjci  32795  atomli  32977  atabs2i  32997  mddmdin0i  33026  imadifxp  33188  fnresin  33211  ofpreima2  33253  df1stres  33290  df2ndres  33291  nn0disj01  33403  dfdec100  33414  decdiv10  33455  dpmul100  33456  dpmul1000  33458  dpexpp1  33467  dpadd2  33469  dpadd  33470  dpmul  33472  dpmul4  33473  threehalves  33474  xrge00  33568  xrge0mulgnn0  33569  cyc2fv1  33675  cyc3conja  33711  elrgspnlem4  33799  xrge0slmod  33902  opprqusplusg  34006  opprqusmulr  34008  selvply1rhmlemb  34144  extvfvcl  34161  2sqr3nconstr  34406  cos9thpiminplylem1  34407  cos9thpiminplylem5  34411  cos9thpinconstrlem2  34415  lmatfvlem  34440  xrge0iifcnv  34558  lmxrge0  34577  cnrrext  34635  qqtopn  34636  esumrnmpt2  34693  esumpfinvallem  34699  unelldsys  34784  ldgenpisyslem1  34789  measunl  34842  mbfmcst  34884  difelcarsg  34935  carsggect  34943  sibfof  34965  eulerpartlemmf  35000  fib2  35027  fib3  35028  fib4  35029  fib5  35030  fib6  35031  0rrv  35076  coinfliprv  35108  ballotlem2  35114  prodfzo03  35225  chtvalz  35251  hgt750lemd  35270  hgt750lem  35273  hgt750lem2  35274  1enumen  35712  kur14lem6  35955  kur14lem7  35956  cvmlift2lem12  36058  problem5  36413  quad3  36414  divcnvlin  36477  in-ax8  36993  bj-2upln1upl  37917  bj-rest0  37994  relowlssretop  38266  relowlpssretop  38267  1oequni2o  38271  curunc  38505  ptrest  38517  poimirlem16  38534  poimirlem30  38548  mblfinlem2  38556  ovoliunnfl  38560  voliunnfl  38562  itg2addnclem2  38570  ftc1anclem5  38595  ftc1anclem6  38596  sdc  38658  heiborlem3  38727  xrnresex  39341  dmxrncnvepres  39344  dvh4dimN  42484  12gcd5e1  43033  60gcd6e6  43034  60gcd7e1  43035  420gcd8e4  43036  lcmeprodgcdi  43037  25or6to4  43236  sq3deccom12  43327  asin1half  43388  acos1half  43389  redvmptabs  43391  readvrec  43393  sn-it1ei  43468  sn-0tie0  43495  dnnumch1  44030  aomclem6  44045  areaquad  44202  naddov4  44369  unitadd  45180  seff  45278  sblpnf  45279  hashnzfz  45289  lhe4.4ex1a  45298  xrtgcntopre  46457  iccdifioo  46496  itgsin0pilem1  46929  stoweidlem13  46992  stoweidlem26  47005  fourierdlem62  47147  fourierdlem102  47187  fourierdlem114  47199  fourierswlem  47209  fouriersw  47210  sge0tsms  47359  meaiuninc  47460  cos5t  47894  goldpolyfactor  47896  goldratval  47905  fmtno4prmfac  48626  41prothprm  48673  ppivalnn4  48681  dfclnbgr4  48891  2zrngasgrp  49312  2zrngmsgrp  49319  tposres3  49958  eloppf  50210  setc1onsubc  50679  dvsec  50825  dvcsc  50826  dvcot  50827  mvlraddi  50836  mvlrmuli  50842  i2linesi  50843  veroquadmodzerod  50953