Theorem eqtr3i 2846

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  3eqtr3i  2852  3eqtr3ri  2853  rabrabi  3494  unundi  4146  unundir  4147  inindi  4203  inindir  4204  dfin4  4244  difun1  4264  difabs  4268  notab  4273  dif0  4332  difdifdir  4437  tpidm13  4686  intmin2  4896  iunxdif3  5010  univ  5336  pwundif  5451  iunxpconst  5619  opabresidOLD  5914  rnresi  5938  rnresv  6053  cnvsn0  6062  resdmres  6084  coi2  6111  coires1  6112  dfdm2  6127  isarep2  6438  resasplit  6543  ssimaex  6743  fnreseql  6813  resfunexg  6972  mpompt  7260  caov31  7371  fvresex  7655  xpexgALT  7676  1st2val  7711  2nd2val  7712  cnvoprab  7752  fnsuppeq0  7852  ecopovtrn  8394  limensuci  8687  pssnn  8730  r1sucg  9192  jech9.3  9237  rankbnd2  9292  djuin  9341  compss  9792  zorn2lem4  9915  iunfo  9955  cardf  9966  alephsuc3  9996  fpwwe2lem13  10058  rankcf  10193  halfnq  10392  addclprlem2  10433  mulgt0sr  10521  mul02lem2  10811  mul02  10812  addid1  10814  mvlladdi  10898  mvllmuli  11467  infrenegsup  11618  8th4div3  11851  nneo  12060  nummac  12137  numadd  12139  numaddc  12140  nummul1c  12141  decbin0  12232  rpsup  13228  resup  13229  om2uzrdg  13318  m1expcl2  13445  facnn  13629  fac0  13630  faclbnd4lem1  13647  4bc3eq4  13682  hasheq0  13718  f1oun2prg  14273  sqrt1  14625  sqrt4  14626  sqrt9  14627  rddif  14694  abs3lemi  14764  sumss2  15077  divcnvshft  15204  geo2sum2  15224  geomulcvg  15226  geoihalfsum  15232  risefall0lem  15374  bpoly2  15405  bpoly3  15406  sin0  15496  efival  15499  ef01bndlem  15531  cos2bnd  15535  sin4lt0  15542  flodddiv4  15758  2prm  16030  unbenlem  16238  dec5dvds  16394  modxai  16398  mod2xi  16399  mod2xnegi  16401  gcdi  16403  numexp2x  16409  decsplit  16413  setsid  16532  mreexexlem3d  16911  oppchom  16979  2oppchomf  16988  isoval  17029  estrres  17383  oppchofcl  17504  oyoncl  17514  mvdco  18567  m1expaddsub  18620  psgn0fv0  18633  oppglsm  18761  dprd2da  19158  ring1  19346  opprsubg  19380  lsppratlem1  19913  ply1basfvi  20403  coe1tm  20435  ply1coe  20458  zzngim  20693  cnmsgnsubg  20715  psgninv  20720  zrhpsgnmhm  20722  neitr  21782  comppfsc  22134  kgeni  22139  xkoinjcn  22289  ufprim  22511  metreslem  22966  restmetu  23174  retopbas  23363  cnfldms  23378  qdensere2  23399  xrsmopn  23414  metdscn2  23459  pcoass  23622  recvs  23744  zclmncvs  23746  iscmet3lem3  23887  cncms  23952  cnfldcusp  23954  resscdrg  23955  rrxprds  23986  ovoliunnul  24102  uniioombllem4  24181  vitalilem5  24207  mbfres  24239  ismbf3d  24249  i1fima  24273  i1fd  24276  itg2cnlem1  24356  itgss3  24409  ellimc2  24469  limccnp2  24484  cpnres  24528  lhop  24607  plyeq0  24795  plypf1  24796  sinhalfpilem  25043  sincos6thpi  25095  sincos3rdpi  25096  pige3ALT  25099  dfrelog  25143  logimul  25191  logneg2  25192  dvlog  25228  cxpsqrt  25280  ang180lem2  25382  ang180lem3  25383  ang180lem4  25384  quart1  25428  asin1  25466  atan0  25480  atanlogsublem  25487  atan1  25500  log2tlbnd  25517  log2ublem2  25519  log2ub  25521  basellem8  25659  cht2  25743  ppiub  25774  bposlem6  25859  bposlem8  25861  bposlem9  25862  lgsdir2lem3  25897  lgseisenlem1  25945  lgseisenlem2  25946  lgsquadlem1  25950  lgsquadlem2  25951  2lgsoddprmlem2  25979  chebbnd1  26042  istrkg3ld  26241  tgcgr4  26311  motplusg  26322  ax5seglem7  26715  ex-un  28197  ex-sqrt  28227  ipdirilem  28600  ipasslem10  28610  hisubcomi  28875  normlem0  28880  norm3difi  28918  norm3lem  28920  polid2i  28928  chdmj1i  29252  chjjdiri  29295  spansn0  29312  pjoml4i  29358  cmbr3i  29371  qlaxr3i  29407  honpcani  29596  honpncani  29598  lnopunilem1  29781  lnophmlem2  29788  lnfn0i  29813  pjbdlni  29920  pjclem1  29966  pjclem3  29968  pjci  29971  atomli  30153  atabs2i  30173  mddmdin0i  30202  disjdifr  30269  difeq  30274  disjdifprg  30319  imadifxp  30345  fnresin  30365  ofpreima2  30405  df1stres  30433  df2ndres  30434  cnvoprabOLD  30450  dfdec100  30541  decdiv10  30567  dpmul100  30568  dpmul1000  30570  dpexpp1  30579  dpadd2  30581  dpadd  30582  dpmul  30584  dpmul4  30585  threehalves  30586  xrge0base  30667  xrge00  30668  xrge0mulgnn0  30671  tocycfvres1  30747  tocycfvres2  30748  cycpmfvlem  30749  cycpmfv3  30752  cycpmcl  30753  cyc2fv1  30758  cyc3conja  30794  xrge0slmod  30912  lmatfvlem  31075  xrge0iifcnv  31171  lmxrge0  31190  cnrrext  31246  qqtopn  31247  esumrnmpt2  31322  esumpfinvallem  31328  unelldsys  31412  ldgenpisyslem1  31417  measunl  31470  mbfmcst  31512  difelcarsg  31563  carsggect  31571  sibfof  31593  eulerpartlemmf  31628  fib2  31655  fib3  31656  fib4  31657  fib5  31658  fib6  31659  0rrv  31704  coinfliprv  31735  ballotlem2  31741  prodfzo03  31869  chtvalz  31895  hgt750lemd  31914  hgt750lem  31917  hgt750lem2  31918  kur14lem6  32453  kur14lem7  32454  cvmlift2lem12  32556  problem5  32907  quad3  32908  divcnvlin  32959  logi  32961  bj-2upln1upl  34331  bj-rest0  34378  relowlssretop  34638  relowlpssretop  34639  1oequni2o  34643  curunc  34868  ptrest  34885  poimirlem16  34902  poimirlem30  34916  mblfinlem2  34924  ovoliunnfl  34928  voliunnfl  34930  itg2addnclem2  34938  ftc1anclem5  34965  ftc1anclem6  34966  sdc  35013  heiborlem3  35085  xrnresex  35648  dvh4dimN  38577  sq3deccom12  39169  dnnumch1  39637  aomclem6  39652  areaquad  39816  unitadd  40541  seff  40634  sblpnf  40635  hashnzfz  40645  lhe4.4ex1a  40654  xrtgcntopre  41747  iccdifioo  41783  itgsin0pilem1  42227  stoweidlem13  42291  stoweidlem26  42304  fourierdlem62  42446  fourierdlem102  42486  fourierdlem114  42498  fourierswlem  42508  fouriersw  42509  sge0tsms  42655  meaiuninc  42756  fmtno4prmfac  43727  41prothprm  43777  2zrngasgrp  44204  2zrngmsgrp  44211  mvlraddi  44864  mvlrmuli  44871  i2linesi  44872