Theorem eqtr3i 2761

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 2745	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2759	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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  3eqtr3i  2767  3eqtr3ri  2768  unundi  4116  unundir  4117  inindi  4175  inindir  4176  dfin4  4218  difun1  4239  difabs  4243  notab  4254  dif0  4318  difdifdir  4431  pwundif  4565  tpidm13  4700  intmin2  4917  iunxdif3  5037  univ  5403  iunxpconst  5704  rnresi  6040  rnresv  6165  cnvsn0  6174  resdmres  6196  coi2  6228  coires1  6229  dfdm2  6245  isarep2  6588  resasplit  6710  ssimaex  6925  fnreseql  7000  resfunexg  7170  mpompt  7481  caov31  7596  fvresex  7913  xpexgALT  7934  1st2val  7970  2nd2val  7971  cnvoprab  8013  fnsuppeq0  8142  ecopovtrn  8767  limensuci  9091  pwfilem  9228  r1sucg  9693  jech9.3  9738  rankbnd2  9793  djuin  9842  compss  10298  zorn2lem4  10421  iunfo  10461  cardf  10472  alephsuc3  10503  fpwwe2lem12  10565  rankcf  10700  halfnq  10899  addclprlem2  10940  mulgt0sr  11028  mul02lem2  11323  mul02  11324  addrid  11326  mvlladdi  11412  mvllmuli  11988  infrenegsup  12139  8th4div3  12397  halfpm6th  12399  nneo  12613  nummac  12689  numadd  12691  numaddc  12692  nummul1c  12693  decbin0  12784  rpsup  13825  resup  13826  om2uzrdg  13918  m1expcl2  14047  facnn  14237  fac0  14238  faclbnd4lem1  14255  4bc3eq4  14290  hasheq0  14325  f1oun2prg  14879  sqrt1  15233  sqrt4  15234  sqrt9  15235  rddif  15303  abs3lemi  15373  sumss2  15688  divcnvshft  15820  geo2sum2  15839  geomulcvg  15841  geoihalfsum  15847  risefall0lem  15991  bpoly2  16022  bpoly3  16023  sin0  16116  efival  16119  ef01bndlem  16151  cos2bnd  16155  sin4lt0  16162  flodddiv4  16384  2prm  16661  unbenlem  16879  dec5dvds  17035  modxai  17039  mod2xi  17040  mod2xnegi  17042  gcdi  17044  numexp2x  17049  decsplit  17053  setsid  17177  xrge0base  17571  mreexexlem3d  17612  oppchom  17681  2oppchomf  17690  isoval  17732  estrres  18105  oppchofcl  18226  oyoncl  18236  mvdco  19420  m1expaddsub  19473  psgn0fv0  19486  oppglsm  19617  dprd2da  20019  ring1  20291  opprsubg  20332  lsppratlem1  21145  pzriprnglem7  21467  zzngim  21532  cnmsgnsubg  21557  psgninv  21562  zrhpsgnmhm  21564  ply1basfvi  22204  coe1tm  22238  ply1coe  22263  comppfsc  23497  kgeni  23502  xkoinjcn  23652  ufprim  23874  metreslem  24327  retopbas  24725  cnfldms  24740  qdensere2  24762  xrsmopn  24778  metdscn2  24823  pcoass  24991  recvs  25113  zclmncvs  25115  iscmet3lem3  25257  cncms  25322  cnfldcusp  25324  resscdrg  25325  rrxprds  25356  ovoliunnul  25474  uniioombllem4  25553  vitalilem5  25579  mbfres  25611  ismbf3d  25621  i1fima  25645  i1fd  25648  itg2cnlem1  25728  itgss3  25782  ellimc2  25844  limccnp2  25859  cpnres  25904  lhop  25983  plyeq0  26176  plypf1  26177  sinhalfpilem  26427  sincos6thpi  26480  sincos3rdpi  26481  pige3ALT  26484  dfrelog  26529  logi  26551  logimul  26578  logneg2  26579  dvlog  26615  cxpsqrt  26667  ang180lem2  26774  ang180lem3  26775  ang180lem4  26776  quart1  26820  asin1  26858  atan0  26872  atanlogsublem  26879  atan1  26892  log2tlbnd  26909  log2ublem2  26911  log2ub  26913  basellem8  27051  cht2  27135  ppiub  27167  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem3  27290  lgseisenlem1  27338  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  2lgsoddprmlem2  27372  chebbnd1  27435  negbdaylem  28048  om2noseqrdg  28296  zseo  28414  bdaypw2n0bndlem  28455  istrkg3ld  28529  tgcgr4  28599  motplusg  28610  ax5seglem7  29004  ex-un  30494  ex-sqrt  30524  ipdirilem  30900  ipasslem10  30910  hisubcomi  31175  normlem0  31180  norm3difi  31218  norm3lem  31220  polid2i  31228  chdmj1i  31552  chjjdiri  31595  spansn0  31612  pjoml4i  31658  cmbr3i  31671  qlaxr3i  31707  honpcani  31896  honpncani  31898  lnopunilem1  32081  lnophmlem2  32088  lnfn0i  32113  pjbdlni  32220  pjclem1  32266  pjclem3  32268  pjci  32271  atomli  32453  atabs2i  32473  mddmdin0i  32502  imadifxp  32671  fnresin  32697  ofpreima2  32739  df1stres  32777  df2ndres  32778  nn0disj01  32892  dfdec100  32903  decdiv10  32955  dpmul100  32956  dpmul1000  32958  dpexpp1  32967  dpadd2  32969  dpadd  32970  dpmul  32972  dpmul4  32973  threehalves  32974  xrge00  33074  xrge0mulgnn0  33075  cyc2fv1  33182  cyc3conja  33218  elrgspnlem4  33306  xrge0slmod  33408  opprqusplusg  33549  opprqusmulr  33551  extvfvcl  33680  2sqr3nconstr  33925  cos9thpiminplylem1  33926  cos9thpiminplylem5  33930  cos9thpinconstrlem2  33934  lmatfvlem  33959  xrge0iifcnv  34077  lmxrge0  34096  cnrrext  34154  qqtopn  34155  esumrnmpt2  34212  esumpfinvallem  34218  unelldsys  34302  ldgenpisyslem1  34307  measunl  34360  mbfmcst  34403  difelcarsg  34454  carsggect  34462  sibfof  34484  eulerpartlemmf  34519  fib2  34546  fib3  34547  fib4  34548  fib5  34549  fib6  34550  0rrv  34595  coinfliprv  34627  ballotlem2  34633  prodfzo03  34747  chtvalz  34773  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  kur14lem6  35393  kur14lem7  35394  cvmlift2lem12  35496  problem5  35851  quad3  35852  divcnvlin  35915  in-ax8  36406  bj-2upln1upl  37331  bj-rest0  37405  relowlssretop  37679  relowlpssretop  37680  1oequni2o  37684  curunc  37923  ptrest  37940  poimirlem16  37957  poimirlem30  37971  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  itg2addnclem2  37993  ftc1anclem5  38018  ftc1anclem6  38019  sdc  38065  heiborlem3  38134  xrnresex  38750  dmxrncnvepres  38753  dvh4dimN  41893  12gcd5e1  42442  60gcd6e6  42443  60gcd7e1  42444  420gcd8e4  42445  lcmeprodgcdi  42446  lcmineqlem23  42490  sq3deccom12  42722  asin1half  42789  acos1half  42790  redvmptabs  42792  readvrec  42794  sn-it1ei  42869  sn-0tie0  42896  dnnumch1  43472  aomclem6  43487  areaquad  43644  naddov4  43811  unitadd  44622  seff  44736  sblpnf  44737  hashnzfz  44747  lhe4.4ex1a  44756  xrtgcntopre  45906  iccdifioo  45945  itgsin0pilem1  46378  stoweidlem13  46441  stoweidlem26  46454  fourierdlem62  46596  fourierdlem102  46636  fourierdlem114  46648  fourierswlem  46658  fouriersw  46659  sge0tsms  46808  meaiuninc  46909  cos5t  47327  fmtno4prmfac  48035  41prothprm  48082  ppivalnn4  48090  dfclnbgr4  48300  2zrngasgrp  48722  2zrngmsgrp  48729  tposres3  49356  eloppf  49608  setc1onsubc  50077  mvlraddi  50246  mvlrmuli  50252  i2linesi  50253