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 2740	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2759	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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  3eqtr3i  2767  3eqtr3ri  2768  rabrabiOLD  3429  unundi  4135  unundir  4136  inindi  4191  inindir  4192  dfin4  4232  difun1  4254  difabs  4258  notab  4269  dif0  4337  disjdifr  4437  difdifdir  4454  pwundif  4589  tpidm13  4722  intmin2  4941  iunxdif3  5060  univ  5413  iunxpconst  5709  rnresi  6032  rnresv  6158  cnvsn0  6167  resdmres  6189  coi2  6220  coires1  6221  dfdm2  6238  isarep2  6597  resasplit  6717  ssimaex  6931  fnreseql  7003  resfunexg  7170  mpompt  7475  caov31  7588  fvresex  7897  xpexgALT  7919  1st2val  7954  2nd2val  7955  cnvoprab  7997  fnsuppeq0  8128  ecopovtrn  8766  limensuci  9104  pwfilem  9128  pssnnOLD  9216  r1sucg  9714  jech9.3  9759  rankbnd2  9814  djuin  9863  compss  10321  zorn2lem4  10444  iunfo  10484  cardf  10495  alephsuc3  10525  fpwwe2lem12  10587  rankcf  10722  halfnq  10921  addclprlem2  10962  mulgt0sr  11050  mul02lem2  11341  mul02  11342  addrid  11344  mvlladdi  11428  mvllmuli  11997  infrenegsup  12147  8th4div3  12382  nneo  12596  nummac  12672  numadd  12674  numaddc  12675  nummul1c  12676  decbin0  12767  rpsup  13781  resup  13782  om2uzrdg  13871  m1expcl2  14001  facnn  14185  fac0  14186  faclbnd4lem1  14203  4bc3eq4  14238  hasheq0  14273  f1oun2prg  14818  sqrt1  15168  sqrt4  15169  sqrt9  15170  rddif  15237  abs3lemi  15307  sumss2  15622  divcnvshft  15751  geo2sum2  15770  geomulcvg  15772  geoihalfsum  15778  risefall0lem  15920  bpoly2  15951  bpoly3  15952  sin0  16042  efival  16045  ef01bndlem  16077  cos2bnd  16081  sin4lt0  16088  flodddiv4  16306  2prm  16579  unbenlem  16791  dec5dvds  16947  modxai  16951  mod2xi  16952  mod2xnegi  16954  gcdi  16956  numexp2x  16962  decsplit  16966  setsid  17091  mreexexlem3d  17540  oppchom  17610  2oppchomf  17620  isoval  17662  estrres  18041  oppchofcl  18163  oyoncl  18173  mvdco  19241  m1expaddsub  19294  psgn0fv0  19307  oppglsm  19438  dprd2da  19835  ring1  20040  opprsubg  20079  lsppratlem1  20667  zzngim  20996  cnmsgnsubg  21018  psgninv  21023  zrhpsgnmhm  21025  ply1basfvi  21649  coe1tm  21681  ply1coe  21704  comppfsc  22920  kgeni  22925  xkoinjcn  23075  ufprim  23297  metreslem  23752  retopbas  24161  cnfldms  24176  qdensere2  24197  xrsmopn  24212  metdscn2  24257  pcoass  24424  recvs  24546  recvsOLD  24547  zclmncvs  24549  iscmet3lem3  24691  cncms  24756  cnfldcusp  24758  resscdrg  24759  rrxprds  24790  ovoliunnul  24908  uniioombllem4  24987  vitalilem5  25013  mbfres  25045  ismbf3d  25055  i1fima  25079  i1fd  25082  itg2cnlem1  25163  itgss3  25216  ellimc2  25278  limccnp2  25293  cpnres  25338  lhop  25417  plyeq0  25609  plypf1  25610  sinhalfpilem  25857  sincos6thpi  25909  sincos3rdpi  25910  pige3ALT  25913  dfrelog  25958  logimul  26006  logneg2  26007  dvlog  26043  cxpsqrt  26095  ang180lem2  26197  ang180lem3  26198  ang180lem4  26199  quart1  26243  asin1  26281  atan0  26295  atanlogsublem  26302  atan1  26315  log2tlbnd  26332  log2ublem2  26334  log2ub  26336  basellem8  26474  cht2  26558  ppiub  26589  bposlem6  26674  bposlem8  26676  bposlem9  26677  lgsdir2lem3  26712  lgseisenlem1  26760  lgseisenlem2  26761  lgsquadlem1  26765  lgsquadlem2  26766  2lgsoddprmlem2  26794  chebbnd1  26857  istrkg3ld  27466  tgcgr4  27536  motplusg  27547  ax5seglem7  27947  ex-un  29431  ex-sqrt  29461  ipdirilem  29834  ipasslem10  29844  hisubcomi  30109  normlem0  30114  norm3difi  30152  norm3lem  30154  polid2i  30162  chdmj1i  30486  chjjdiri  30529  spansn0  30546  pjoml4i  30592  cmbr3i  30605  qlaxr3i  30641  honpcani  30830  honpncani  30832  lnopunilem1  31015  lnophmlem2  31022  lnfn0i  31047  pjbdlni  31154  pjclem1  31200  pjclem3  31202  pjci  31205  atomli  31387  atabs2i  31407  mddmdin0i  31436  imadifxp  31586  fnresin  31607  ofpreima2  31649  df1stres  31685  df2ndres  31686  cnvoprabOLD  31705  dfdec100  31796  decdiv10  31822  dpmul100  31823  dpmul1000  31825  dpexpp1  31834  dpadd2  31836  dpadd  31837  dpmul  31839  dpmul4  31840  threehalves  31841  xrge0base  31946  xrge00  31947  xrge0mulgnn0  31950  cyc2fv1  32040  cyc3conja  32076  xrge0slmod  32211  lmatfvlem  32485  xrge0iifcnv  32603  lmxrge0  32622  cnrrext  32680  qqtopn  32681  esumrnmpt2  32756  esumpfinvallem  32762  unelldsys  32846  ldgenpisyslem1  32851  measunl  32904  mbfmcst  32948  difelcarsg  32999  carsggect  33007  sibfof  33029  eulerpartlemmf  33064  fib2  33091  fib3  33092  fib4  33093  fib5  33094  fib6  33095  0rrv  33140  coinfliprv  33171  ballotlem2  33177  prodfzo03  33305  chtvalz  33331  hgt750lemd  33350  hgt750lem  33353  hgt750lem2  33354  kur14lem6  33892  kur14lem7  33893  cvmlift2lem12  33995  problem5  34344  quad3  34345  divcnvlin  34391  logi  34393  bj-2upln1upl  35568  bj-rest0  35637  relowlssretop  35907  relowlpssretop  35908  1oequni2o  35912  curunc  36133  ptrest  36150  poimirlem16  36167  poimirlem30  36181  mblfinlem2  36189  ovoliunnfl  36193  voliunnfl  36195  itg2addnclem2  36203  ftc1anclem5  36228  ftc1anclem6  36229  sdc  36276  heiborlem3  36345  xrnresex  36941  dvh4dimN  39983  12gcd5e1  40533  60gcd6e6  40534  60gcd7e1  40535  420gcd8e4  40536  lcmeprodgcdi  40537  lcmineqlem23  40581  acos1half  40695  sq3deccom12  40862  it1ei  40963  sn-0tie0  40966  sn-inelr  40992  dnnumch1  41429  aomclem6  41444  areaquad  41608  naddov4  41776  unitadd  42590  seff  42711  sblpnf  42712  hashnzfz  42722  lhe4.4ex1a  42731  xrtgcntopre  43834  iccdifioo  43873  itgsin0pilem1  44311  stoweidlem13  44374  stoweidlem26  44387  fourierdlem62  44529  fourierdlem102  44569  fourierdlem114  44581  fourierswlem  44591  fouriersw  44592  sge0tsms  44741  meaiuninc  44842  tworepnotupword  45245  fmtno4prmfac  45884  41prothprm  45931  2zrngasgrp  46358  2zrngmsgrp  46365  mvlraddi  47337  mvlrmuli  47344  i2linesi  47345