Theorem eqtr3i 2634

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  3eqtr3i  2640  3eqtr3ri  2641  unundi  3736  unundir  3737  inindi  3792  inindir  3793  dfin4  3826  difun1  3846  difabs  3851  notab  3856  dif0  3904  difdifdir  4008  tpidm13  4235  intmin2  4439  iunxdif3  4542  univ  4846  iunxpconst  5098  dmres  5339  opabresid  5374  rnresi  5398  cnvcnv  5505  rnresv  5512  cnvsn0  5521  cnvsn  5536  resdmres  5543  coi2  5569  coires1  5570  dfdm2  5584  isarep2  5892  resasplit  5987  ssimaex  6173  fnreseql  6235  resfunexg  6384  idref  6403  mpt2mpt  6650  caov31  6761  fvresex  7032  xpexgALT  7052  1st2val  7085  2nd2val  7086  fnsuppeq0  7210  ecopovtrn  7737  limensuci  8021  pssnn  8063  r1sucg  8515  jech9.3  8560  rankbnd2  8615  compss  9081  zorn2lem4  9204  iunfo  9240  cardf  9251  alephsuc3  9281  fpwwe2lem13  9343  rankcf  9478  halfnq  9677  addclprlem2  9718  mulgt0sr  9805  mul02lem2  10092  mul02  10093  addid1  10095  mvlladdi  10178  mvllmuli  10737  infrenegsup  10883  8th4div3  11129  nneo  11337  dec10OLD  11431  nummac  11434  numadd  11436  numaddc  11437  nummul1c  11438  9p2e11OLD  11496  decbin0  11558  rpsup  12527  resup  12528  om2uzrdg  12617  m1expcl2  12744  facnn  12924  fac0  12925  faclbnd4lem1  12942  4bc3eq4  12977  hasheq0  13015  f1oun2prg  13512  sqrt1  13860  sqrt4  13861  sqrt9  13862  rddif  13928  abs3lemi  13997  sumss2  14304  divcnvshft  14426  geo2sum2  14444  geomulcvg  14446  geoihalfsum  14453  risefall0lem  14596  bpoly2  14627  bpoly3  14628  sin0  14718  efival  14721  ef01bndlem  14753  cos2bnd  14757  sin4lt0  14764  flodddiv4  14975  2prm  15243  unbenlem  15450  dec5dvds  15606  modxai  15610  mod2xi  15611  mod2xnegi  15613  gcdi  15615  numexp2x  15621  decsplit  15625  decsplitOLD  15629  setsid  15742  mreexexlem3d  16129  oppchom  16198  2oppchomf  16207  isoval  16248  estrres  16602  oppchofcl  16723  oyoncl  16733  mvdco  17688  m1expaddsub  17741  psgn0fv0  17754  oppglsm  17880  dprd2da  18264  ring1  18425  opprsubg  18459  lsppratlem1  18968  opsrtoslem1  19305  ply1basfvi  19432  coe1tm  19464  ply1coe  19487  zzngim  19720  cnmsgnsubg  19742  psgninv  19747  zrhpsgnmhm  19749  neitr  20794  comppfsc  21145  kgeni  21150  xkoinjcn  21300  ufprim  21523  metreslem  21977  restmetu  22185  retopbas  22374  cnfldms  22389  qdensere2  22408  xrsmopn  22423  metdscn2  22468  pcoass  22632  recvs  22754  zclmncvs  22756  iscmet3lem3  22896  cncms  22959  cnfldcusp  22961  resscdrg  22962  rrxprds  22985  ovoliunnul  23082  uniioombllem4  23160  vitalilem5  23187  mbfres  23217  ismbf3d  23227  i1fima  23251  i1fd  23254  itg2cnlem1  23334  itgss3  23387  ellimc2  23447  limccnp2  23462  cpnres  23506  lhop  23583  plyeq0  23771  plypf1  23772  sinhalfpilem  24019  sincos6thpi  24071  sincos3rdpi  24072  pige3  24073  dfrelog  24116  logimul  24164  logneg2  24165  dvlog  24197  cxpsqrt  24249  ang180lem2  24340  ang180lem3  24341  ang180lem4  24342  quart1  24383  asin1  24421  atan0  24435  atanlogsublem  24442  atan1  24455  log2tlbnd  24472  log2ublem2  24474  log2ub  24476  basellem8  24614  cht2  24698  ppiub  24729  bposlem6  24814  bposlem8  24816  bposlem9  24817  lgsdir2lem3  24852  lgseisenlem1  24900  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  2lgsoddprmlem2  24934  chebbnd1  24961  istrkg3ld  25160  tgcgr4  25226  motplusg  25237  ax5seglem7  25615  ex-un  26673  ex-sqrt  26703  ipdirilem  27068  ipasslem10  27078  hisubcomi  27345  normlem0  27350  norm3difi  27388  norm3lem  27390  polid2i  27398  chdmj1i  27724  chjjdiri  27767  spansn0  27784  pjoml4i  27830  cmbr3i  27843  qlaxr3i  27879  honpcani  28068  honpncani  28070  lnopunilem1  28253  lnophmlem2  28260  lnfn0i  28285  pjbdlni  28392  pjclem1  28438  pjclem3  28440  pjci  28443  atomli  28625  atabs2i  28645  mddmdin0i  28674  difeq  28739  disjdifprg  28770  imadifxp  28796  fnresin  28812  ofpreima2  28849  df1stres  28864  df2ndres  28865  cnvoprab  28886  xrge0base  29016  xrge00  29017  xrge0mulgnn0  29020  xrge0slmod  29175  lmatfvlem  29209  xrge0iifcnv  29307  lmxrge0  29326  cnrrext  29382  qqtopn  29383  esumrnmpt2  29457  esumpfinvallem  29463  unelldsys  29548  ldgenpisyslem1  29553  measunl  29606  mbfmcst  29648  difelcarsg  29699  carsggect  29707  sibfof  29729  eulerpartlemmf  29764  fib2  29791  fib3  29792  fib4  29793  fib5  29794  fib6  29795  0rrv  29840  coinfliprv  29871  ballotlem2  29877  kur14lem6  30447  kur14lem7  30448  cvmlift2lem12  30550  problem5  30817  quad3  30818  divcnvlin  30871  logi  30873  bj-2upln1upl  32205  bj-rest0  32227  relowlssretop  32387  relowlpssretop  32388  1oequni2o  32392  curunc  32561  ptrest  32578  poimirlem16  32595  poimirlem30  32609  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  itg2addnclem2  32632  ftc1anclem5  32659  ftc1anclem6  32660  sdc  32710  heiborlem3  32782  dvh4dimN  35754  dnnumch1  36632  aomclem6  36647  areaquad  36821  unitadd  37520  seff  37530  sblpnf  37531  hashnzfz  37541  lhe4.4ex1a  37550  iccdifioo  38588  itgsin0pilem1  38841  stoweidlem13  38906  stoweidlem26  38919  fourierdlem62  39061  fourierdlem102  39101  fourierdlem114  39113  fourierswlem  39123  fouriersw  39124  sge0tsms  39273  meaiuninc  39374  fmtno4prmfac  40022  41prothprm  40074  2zrngasgrp  41730  2zrngmsgrp  41737  mvlraddi  42323  mvlrmuli  42332  i2linesi  42333