Theorem eqtr3i 2785

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 2769	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2783	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 2732

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

This theorem is used by:  3eqtr3i  2791  3eqtr3ri  2792  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  5426  iunxpconst  5728  resdmdfsn  6025  rnresi  6071  rnresv  6195  imadifssran  6197  cnvsn0  6206  resdmres  6228  coi2  6260  coires1  6261  dfdm2  6279  isarep2  6622  resasplit  6745  ssimaex  6963  fnreseql  7040  resfunexg  7214  mpompt  7527  caov31  7643  fvresex  7957  xpexgALT  7978  1st2val  8014  2nd2val  8015  cnvoprab  8057  fnsuppeq0  8190  ecopovtrn  8820  limensuci  9151  pwfilem  9287  r1sucg  9751  jech9.3  9796  rankbnd2  9851  djuin  9923  compss  10378  zorn2lem4  10501  iunfo  10547  cardf  10558  alephsuc3  10589  fpwwe2lem12  10651  rankcf  10786  halfnq  10985  addclprlem2  11026  mulgt0sr  11114  mul02lem2  11411  mul02  11412  addrid  11414  mvlladdi  11500  mvllmuli  12072  infrenegsup  12222  halfpm6th  12490  nneo  12705  nummac  12786  numadd  12788  numaddc  12789  nummul1c  12790  decbin0  12883  fz00m1  13600  rpsup  13927  resup  13928  om2uzrdg  14020  m1expcl2  14149  facnn  14339  fac0  14340  faclbnd4lem1  14357  4bc3eq4  14392  hasheq0  14427  f1oun2prg  14988  sqrt1  15358  sqrt4  15359  sqrt9  15360  rddif  15428  abs3lemi  15498  sumss2  15812  divcnvshft  15944  geo2sum2  15963  geomulcvg  15965  geoihalfsum  15971  bpoly2  16143  bpoly3  16144  sin0  16237  efival  16240  ef01bndlem  16272  cos2bnd  16276  sin4lt0  16283  flodddiv4  16505  2prm  16782  unbenlem  17000  dec5dvds  17156  modxai  17160  mod2xi  17161  mod2xnegi  17163  gcdi  17165  numexp2x  17170  decsplit  17174  setsid  17299  xrge0base  17693  mreexexlem3d  17734  oppchom  17803  2oppchomf  17812  isoval  17854  estrres  18227  oppchofcl  18348  oyoncl  18358  mvdco  19572  m1expaddsub  19625  psgn0fv0  19638  oppglsm  19769  dprd2da  20171  ring1  20452  opprsubg  20493  lsppratlem1  21334  pzriprnglem7  21700  zzngim  21765  cnmsgnsubg  21790  psgninv  21795  zrhpsgnmhm  21797  ply1basfvi  22465  coe1tm  22499  ply1coe  22523  comppfsc  23758  kgeni  23763  xkoinjcn  23913  ufprim  24135  metreslem  24588  retopbas  24986  cnfldms  25001  qdensere2  25023  xrsmopn  25039  metdscn2  25084  pcoass  25252  recvs  25374  zclmncvs  25376  iscmet3lem3  25518  cncms  25583  cnfldcusp  25585  resscdrg  25586  rrxprds  25617  ovoliunnul  25735  uniioombllem4  25814  vitalilem5  25840  mbfres  25872  ismbf3d  25882  i1fima  25906  i1fd  25909  itg2cnlem1  25989  itgss3  26042  ellimc2  26104  limccnp2  26119  cpnres  26164  lhop  26243  plyeq0  26437  plypf1  26438  sinhalfpilem  26701  sincos6thpi  26753  sincos3rdpi  26754  pige3ALT  26757  dfrelog  26802  logi  26824  logimul  26851  logneg2  26852  dvlog  26888  cxpsqrt  26940  ang180lem2  27047  ang180lem3  27048  ang180lem4  27049  quart1  27093  asin1  27131  atan0  27145  atanlogsublem  27152  atan1  27165  log2tlbnd  27182  log2ublem2  27184  log2ub  27186  cht2  27408  ppiub  27440  bposlem6  27525  bposlem8  27527  bposlem9  27528  lgsdir2lem3  27563  lgseisenlem1  27611  lgseisenlem2  27612  lgsquadlem1  27616  lgsquadlem2  27617  2lgsoddprmlem2  27645  chebbnd1  27708  negbdaylem  28321  om2noseqrdg  28569  zseo  28687  bdaypw2n0bndlem  28728  istrkg3ld  28802  tgcgr4  28873  motplusg  28884  ax5seglem7  29392  ex-un  30904  ex-sqrt  30934  ipdirilem  31310  ipasslem10  31320  hisubcomi  31585  normlem0  31590  norm3difi  31628  norm3lem  31630  polid2i  31638  chdmj1i  31962  chjjdiri  32005  spansn0  32022  pjoml4i  32068  cmbr3i  32081  qlaxr3i  32117  honpcani  32306  honpncani  32308  lnopunilem1  32491  lnophmlem2  32498  lnfn0i  32523  pjbdlni  32630  pjclem1  32676  pjclem3  32678  pjci  32681  atomli  32863  atabs2i  32883  mddmdin0i  32912  imadifxp  33074  fnresin  33097  ofpreima2  33139  df1stres  33176  df2ndres  33177  nn0disj01  33289  dfdec100  33300  decdiv10  33341  dpmul100  33342  dpmul1000  33344  dpexpp1  33353  dpadd2  33355  dpadd  33356  dpmul  33358  dpmul4  33359  threehalves  33360  xrge00  33454  xrge0mulgnn0  33455  cyc2fv1  33561  cyc3conja  33597  elrgspnlem4  33685  xrge0slmod  33788  opprqusplusg  33891  opprqusmulr  33893  selvply1rhmlemb  34029  extvfvcl  34046  2sqr3nconstr  34291  cos9thpiminplylem1  34292  cos9thpiminplylem5  34296  cos9thpinconstrlem2  34300  lmatfvlem  34325  xrge0iifcnv  34443  lmxrge0  34462  cnrrext  34520  qqtopn  34521  esumrnmpt2  34578  esumpfinvallem  34584  unelldsys  34669  ldgenpisyslem1  34674  measunl  34727  mbfmcst  34770  difelcarsg  34821  carsggect  34829  sibfof  34851  eulerpartlemmf  34886  fib2  34913  fib3  34914  fib4  34915  fib5  34916  fib6  34917  0rrv  34962  coinfliprv  34994  ballotlem2  35000  prodfzo03  35111  chtvalz  35137  hgt750lemd  35156  hgt750lem  35159  hgt750lem2  35160  1enumen  35599  kur14lem6  35790  kur14lem7  35791  cvmlift2lem12  35893  problem5  36248  quad3  36249  divcnvlin  36312  in-ax8  36844  bj-2upln1upl  37768  bj-rest0  37843  relowlssretop  38117  relowlpssretop  38118  1oequni2o  38122  curunc  38356  ptrest  38368  poimirlem16  38385  poimirlem30  38399  mblfinlem2  38407  ovoliunnfl  38411  voliunnfl  38413  itg2addnclem2  38421  ftc1anclem5  38446  ftc1anclem6  38447  sdc  38494  heiborlem3  38563  xrnresex  39177  dmxrncnvepres  39180  dvh4dimN  42320  12gcd5e1  42869  60gcd6e6  42870  60gcd7e1  42871  420gcd8e4  42872  lcmeprodgcdi  42873  25or6to4  43072  sq3deccom12  43165  asin1half  43232  acos1half  43233  redvmptabs  43235  readvrec  43237  sn-it1ei  43312  sn-0tie0  43339  dnnumch1  43885  aomclem6  43900  areaquad  44057  naddov4  44224  unitadd  45035  seff  45133  sblpnf  45134  hashnzfz  45144  lhe4.4ex1a  45153  xrtgcntopre  46306  iccdifioo  46345  itgsin0pilem1  46778  stoweidlem13  46841  stoweidlem26  46854  fourierdlem62  46996  fourierdlem102  47036  fourierdlem114  47048  fourierswlem  47058  fouriersw  47059  sge0tsms  47208  meaiuninc  47309  cos5t  47743  goldpolyfactor  47745  goldratval  47754  fmtno4prmfac  48475  41prothprm  48522  ppivalnn4  48530  dfclnbgr4  48740  2zrngasgrp  49161  2zrngmsgrp  49168  tposres3  49807  eloppf  50059  setc1onsubc  50528  dvsec  50689  dvcsc  50690  dvcot  50691  mvlraddi  50700  mvlrmuli  50706  i2linesi  50707  veroquadmodzerod  50817