Theorem eqtr3i 2759

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  3eqtr3i  2765  3eqtr3ri  2766  unundi  4126  unundir  4127  inindi  4185  inindir  4186  dfin4  4228  difun1  4249  difabs  4253  notab  4264  dif0  4328  disjdifr  4423  difdifdir  4442  pwundif  4576  tpidm13  4711  intmin2  4928  iunxdif3  5048  univ  5397  iunxpconst  5695  rnresi  6032  rnresv  6157  cnvsn0  6166  resdmres  6188  coi2  6220  coires1  6221  dfdm2  6237  isarep2  6580  resasplit  6702  ssimaex  6917  fnreseql  6991  resfunexg  7159  mpompt  7470  caov31  7585  fvresex  7902  xpexgALT  7923  1st2val  7959  2nd2val  7960  cnvoprab  8002  fnsuppeq0  8132  ecopovtrn  8755  limensuci  9079  pwfilem  9216  r1sucg  9679  jech9.3  9724  rankbnd2  9779  djuin  9828  compss  10284  zorn2lem4  10407  iunfo  10447  cardf  10458  alephsuc3  10489  fpwwe2lem12  10551  rankcf  10686  halfnq  10885  addclprlem2  10926  mulgt0sr  11014  mul02lem2  11308  mul02  11309  addrid  11311  mvlladdi  11397  mvllmuli  11972  infrenegsup  12123  8th4div3  12359  halfpm6th  12361  nneo  12574  nummac  12650  numadd  12652  numaddc  12653  nummul1c  12654  decbin0  12745  rpsup  13784  resup  13785  om2uzrdg  13877  m1expcl2  14006  facnn  14196  fac0  14197  faclbnd4lem1  14214  4bc3eq4  14249  hasheq0  14284  f1oun2prg  14838  sqrt1  15192  sqrt4  15193  sqrt9  15194  rddif  15262  abs3lemi  15332  sumss2  15647  divcnvshft  15776  geo2sum2  15795  geomulcvg  15797  geoihalfsum  15803  risefall0lem  15947  bpoly2  15978  bpoly3  15979  sin0  16072  efival  16075  ef01bndlem  16107  cos2bnd  16111  sin4lt0  16118  flodddiv4  16340  2prm  16617  unbenlem  16834  dec5dvds  16990  modxai  16994  mod2xi  16995  mod2xnegi  16997  gcdi  16999  numexp2x  17004  decsplit  17008  setsid  17132  xrge0base  17526  mreexexlem3d  17567  oppchom  17636  2oppchomf  17645  isoval  17687  estrres  18060  oppchofcl  18181  oyoncl  18191  mvdco  19372  m1expaddsub  19425  psgn0fv0  19438  oppglsm  19569  dprd2da  19971  ring1  20243  opprsubg  20286  lsppratlem1  21100  pzriprnglem7  21440  zzngim  21505  cnmsgnsubg  21530  psgninv  21535  zrhpsgnmhm  21537  ply1basfvi  22179  coe1tm  22213  ply1coe  22240  comppfsc  23474  kgeni  23479  xkoinjcn  23629  ufprim  23851  metreslem  24304  retopbas  24702  cnfldms  24717  qdensere2  24739  xrsmopn  24755  metdscn2  24800  pcoass  24978  recvs  25100  zclmncvs  25102  iscmet3lem3  25244  cncms  25309  cnfldcusp  25311  resscdrg  25312  rrxprds  25343  ovoliunnul  25462  uniioombllem4  25541  vitalilem5  25567  mbfres  25599  ismbf3d  25609  i1fima  25633  i1fd  25636  itg2cnlem1  25716  itgss3  25770  ellimc2  25832  limccnp2  25847  cpnres  25893  lhop  25975  plyeq0  26170  plypf1  26171  sinhalfpilem  26426  sincos6thpi  26479  sincos3rdpi  26480  pige3ALT  26483  dfrelog  26528  logi  26550  logimul  26577  logneg2  26578  dvlog  26614  cxpsqrt  26666  ang180lem2  26774  ang180lem3  26775  ang180lem4  26776  quart1  26820  asin1  26858  atan0  26872  atanlogsublem  26879  atan1  26892  log2tlbnd  26909  log2ublem2  26911  log2ub  26913  basellem8  27052  cht2  27136  ppiub  27169  bposlem6  27254  bposlem8  27256  bposlem9  27257  lgsdir2lem3  27292  lgseisenlem1  27340  lgseisenlem2  27341  lgsquadlem1  27345  lgsquadlem2  27346  2lgsoddprmlem2  27374  chebbnd1  27437  negsbdaylem  28025  om2noseqrdg  28265  zseo  28380  bdaypw2n0s  28420  istrkg3ld  28482  tgcgr4  28552  motplusg  28563  ax5seglem7  28957  ex-un  30448  ex-sqrt  30478  ipdirilem  30853  ipasslem10  30863  hisubcomi  31128  normlem0  31133  norm3difi  31171  norm3lem  31173  polid2i  31181  chdmj1i  31505  chjjdiri  31548  spansn0  31565  pjoml4i  31611  cmbr3i  31624  qlaxr3i  31660  honpcani  31849  honpncani  31851  lnopunilem1  32034  lnophmlem2  32041  lnfn0i  32066  pjbdlni  32173  pjclem1  32219  pjclem3  32221  pjci  32224  atomli  32406  atabs2i  32426  mddmdin0i  32455  imadifxp  32625  fnresin  32651  ofpreima2  32693  df1stres  32732  df2ndres  32733  nn0disj01  32848  dfdec100  32860  decdiv10  32926  dpmul100  32927  dpmul1000  32929  dpexpp1  32938  dpadd2  32940  dpadd  32941  dpmul  32943  dpmul4  32944  threehalves  32945  xrge00  33045  xrge0mulgnn0  33046  cyc2fv1  33152  cyc3conja  33188  elrgspnlem4  33276  xrge0slmod  33378  opprqusplusg  33519  opprqusmulr  33521  extvfvcl  33650  2sqr3nconstr  33887  cos9thpiminplylem1  33888  cos9thpiminplylem5  33892  cos9thpinconstrlem2  33896  lmatfvlem  33921  xrge0iifcnv  34039  lmxrge0  34058  cnrrext  34116  qqtopn  34117  esumrnmpt2  34174  esumpfinvallem  34180  unelldsys  34264  ldgenpisyslem1  34269  measunl  34322  mbfmcst  34365  difelcarsg  34416  carsggect  34424  sibfof  34446  eulerpartlemmf  34481  fib2  34508  fib3  34509  fib4  34510  fib5  34511  fib6  34512  0rrv  34557  coinfliprv  34589  ballotlem2  34595  prodfzo03  34709  chtvalz  34735  hgt750lemd  34754  hgt750lem  34757  hgt750lem2  34758  kur14lem6  35354  kur14lem7  35355  cvmlift2lem12  35457  problem5  35812  quad3  35813  divcnvlin  35876  in-ax8  36367  bj-2upln1upl  37168  bj-rest0  37237  relowlssretop  37507  relowlpssretop  37508  1oequni2o  37512  curunc  37742  ptrest  37759  poimirlem16  37776  poimirlem30  37790  mblfinlem2  37798  ovoliunnfl  37802  voliunnfl  37804  itg2addnclem2  37812  ftc1anclem5  37837  ftc1anclem6  37838  sdc  37884  heiborlem3  37953  xrnresex  38553  dmxrncnvepres  38556  dvh4dimN  41646  12gcd5e1  42196  60gcd6e6  42197  60gcd7e1  42198  420gcd8e4  42199  lcmeprodgcdi  42200  lcmineqlem23  42244  sq3deccom12  42487  asin1half  42554  acos1half  42555  redvmptabs  42557  readvrec  42559  sn-it1ei  42634  sn-0tie0  42648  dnnumch1  43228  aomclem6  43243  areaquad  43400  naddov4  43567  unitadd  44378  seff  44492  sblpnf  44493  hashnzfz  44503  lhe4.4ex1a  44512  xrtgcntopre  45664  iccdifioo  45703  itgsin0pilem1  46136  stoweidlem13  46199  stoweidlem26  46212  fourierdlem62  46354  fourierdlem102  46394  fourierdlem114  46406  fourierswlem  46416  fouriersw  46417  sge0tsms  46566  meaiuninc  46667  fmtno4prmfac  47760  41prothprm  47807  dfclnbgr4  48012  2zrngasgrp  48434  2zrngmsgrp  48441  tposres3  49068  eloppf  49320  setc1onsubc  49789  mvlraddi  49958  mvlrmuli  49964  i2linesi  49965