Theorem eqtr3i 2848

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

Syntax hints:   = wceq 1537

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 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  3eqtr3i  2854  3eqtr3ri  2855  rabrabi  3495  unundi  4148  unundir  4149  inindi  4205  inindir  4206  dfin4  4246  difun1  4266  difabs  4270  notab  4275  dif0  4334  difdifdir  4439  pwundif  4567  tpidm13  4694  intmin2  4905  iunxdif3  5019  univ  5346  iunxpconst  5626  opabresidOLD  5921  rnresi  5945  rnresv  6060  cnvsn0  6069  resdmres  6091  coi2  6118  coires1  6119  dfdm2  6134  isarep2  6445  resasplit  6550  ssimaex  6750  fnreseql  6820  resfunexg  6980  mpompt  7268  caov31  7379  fvresex  7663  xpexgALT  7684  1st2val  7719  2nd2val  7720  cnvoprab  7760  fnsuppeq0  7860  ecopovtrn  8402  limensuci  8695  pssnn  8738  r1sucg  9200  jech9.3  9245  rankbnd2  9300  djuin  9349  compss  9800  zorn2lem4  9923  iunfo  9963  cardf  9974  alephsuc3  10004  fpwwe2lem13  10066  rankcf  10201  halfnq  10400  addclprlem2  10441  mulgt0sr  10529  mul02lem2  10819  mul02  10820  addid1  10822  mvlladdi  10906  mvllmuli  11475  infrenegsup  11626  8th4div3  11860  nneo  12069  nummac  12146  numadd  12148  numaddc  12149  nummul1c  12150  decbin0  12241  rpsup  13237  resup  13238  om2uzrdg  13327  m1expcl2  13454  facnn  13638  fac0  13639  faclbnd4lem1  13656  4bc3eq4  13691  hasheq0  13727  f1oun2prg  14281  sqrt1  14633  sqrt4  14634  sqrt9  14635  rddif  14702  abs3lemi  14772  sumss2  15085  divcnvshft  15212  geo2sum2  15232  geomulcvg  15234  geoihalfsum  15240  risefall0lem  15382  bpoly2  15413  bpoly3  15414  sin0  15504  efival  15507  ef01bndlem  15539  cos2bnd  15543  sin4lt0  15550  flodddiv4  15766  2prm  16038  unbenlem  16246  dec5dvds  16402  modxai  16406  mod2xi  16407  mod2xnegi  16409  gcdi  16411  numexp2x  16417  decsplit  16421  setsid  16540  mreexexlem3d  16919  oppchom  16987  2oppchomf  16996  isoval  17037  estrres  17391  oppchofcl  17512  oyoncl  17522  mvdco  18575  m1expaddsub  18628  psgn0fv0  18641  oppglsm  18769  dprd2da  19166  ring1  19354  opprsubg  19388  lsppratlem1  19921  ply1basfvi  20411  coe1tm  20443  ply1coe  20466  zzngim  20701  cnmsgnsubg  20723  psgninv  20728  zrhpsgnmhm  20730  neitr  21790  comppfsc  22142  kgeni  22147  xkoinjcn  22297  ufprim  22519  metreslem  22974  restmetu  23182  retopbas  23371  cnfldms  23386  qdensere2  23407  xrsmopn  23422  metdscn2  23467  pcoass  23630  recvs  23752  zclmncvs  23754  iscmet3lem3  23895  cncms  23960  cnfldcusp  23962  resscdrg  23963  rrxprds  23994  ovoliunnul  24110  uniioombllem4  24189  vitalilem5  24215  mbfres  24247  ismbf3d  24257  i1fima  24281  i1fd  24284  itg2cnlem1  24364  itgss3  24417  ellimc2  24477  limccnp2  24492  cpnres  24536  lhop  24615  plyeq0  24803  plypf1  24804  sinhalfpilem  25051  sincos6thpi  25103  sincos3rdpi  25104  pige3ALT  25107  dfrelog  25151  logimul  25199  logneg2  25200  dvlog  25236  cxpsqrt  25288  ang180lem2  25390  ang180lem3  25391  ang180lem4  25392  quart1  25436  asin1  25474  atan0  25488  atanlogsublem  25495  atan1  25508  log2tlbnd  25525  log2ublem2  25527  log2ub  25529  basellem8  25667  cht2  25751  ppiub  25782  bposlem6  25867  bposlem8  25869  bposlem9  25870  lgsdir2lem3  25905  lgseisenlem1  25953  lgseisenlem2  25954  lgsquadlem1  25958  lgsquadlem2  25959  2lgsoddprmlem2  25987  chebbnd1  26050  istrkg3ld  26249  tgcgr4  26319  motplusg  26330  ax5seglem7  26723  ex-un  28205  ex-sqrt  28235  ipdirilem  28608  ipasslem10  28618  hisubcomi  28883  normlem0  28888  norm3difi  28926  norm3lem  28928  polid2i  28936  chdmj1i  29260  chjjdiri  29303  spansn0  29320  pjoml4i  29366  cmbr3i  29379  qlaxr3i  29415  honpcani  29604  honpncani  29606  lnopunilem1  29789  lnophmlem2  29796  lnfn0i  29821  pjbdlni  29928  pjclem1  29974  pjclem3  29976  pjci  29979  atomli  30161  atabs2i  30181  mddmdin0i  30210  disjdifr  30277  difeq  30282  disjdifprg  30327  imadifxp  30353  fnresin  30373  ofpreima2  30413  df1stres  30441  df2ndres  30442  cnvoprabOLD  30458  dfdec100  30548  decdiv10  30574  dpmul100  30575  dpmul1000  30577  dpexpp1  30586  dpadd2  30588  dpadd  30589  dpmul  30591  dpmul4  30592  threehalves  30593  xrge0base  30674  xrge00  30675  xrge0mulgnn0  30678  tocycfvres1  30754  tocycfvres2  30755  cycpmfvlem  30756  cycpmfv3  30759  cycpmcl  30760  cyc2fv1  30765  cyc3conja  30801  xrge0slmod  30919  lmatfvlem  31082  xrge0iifcnv  31178  lmxrge0  31197  cnrrext  31253  qqtopn  31254  esumrnmpt2  31329  esumpfinvallem  31335  unelldsys  31419  ldgenpisyslem1  31424  measunl  31477  mbfmcst  31519  difelcarsg  31570  carsggect  31578  sibfof  31600  eulerpartlemmf  31635  fib2  31662  fib3  31663  fib4  31664  fib5  31665  fib6  31666  0rrv  31711  coinfliprv  31742  ballotlem2  31748  prodfzo03  31876  chtvalz  31902  hgt750lemd  31921  hgt750lem  31924  hgt750lem2  31925  kur14lem6  32460  kur14lem7  32461  cvmlift2lem12  32563  problem5  32914  quad3  32915  divcnvlin  32966  logi  32968  bj-2upln1upl  34338  bj-rest0  34386  relowlssretop  34646  relowlpssretop  34647  1oequni2o  34651  curunc  34876  ptrest  34893  poimirlem16  34910  poimirlem30  34924  mblfinlem2  34932  ovoliunnfl  34936  voliunnfl  34938  itg2addnclem2  34946  ftc1anclem5  34973  ftc1anclem6  34974  sdc  35021  heiborlem3  35093  xrnresex  35656  dvh4dimN  38585  sq3deccom12  39183  dnnumch1  39651  aomclem6  39666  areaquad  39830  unitadd  40555  seff  40648  sblpnf  40649  hashnzfz  40659  lhe4.4ex1a  40668  xrtgcntopre  41762  iccdifioo  41798  itgsin0pilem1  42242  stoweidlem13  42305  stoweidlem26  42318  fourierdlem62  42460  fourierdlem102  42500  fourierdlem114  42512  fourierswlem  42522  fouriersw  42523  sge0tsms  42669  meaiuninc  42770  fmtno4prmfac  43741  41prothprm  43791  2zrngasgrp  44218  2zrngmsgrp  44225  mvlraddi  44878  mvlrmuli  44885  i2linesi  44886