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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728

This theorem is referenced by:  3eqtr3i  2767  3eqtr3ri  2768  unundi  4156  unundir  4157  inindi  4215  inindir  4216  dfin4  4258  difun1  4279  difabs  4283  notab  4294  dif0  4358  disjdifr  4453  difdifdir  4472  pwundif  4604  tpidm13  4737  intmin2  4956  iunxdif3  5076  univ  5431  iunxpconst  5732  rnresi  6067  rnresv  6195  cnvsn0  6204  resdmres  6226  coi2  6257  coires1  6258  dfdm2  6275  isarep2  6633  resasplit  6753  ssimaex  6969  fnreseql  7043  resfunexg  7212  mpompt  7526  caov31  7641  fvresex  7963  xpexgALT  7985  1st2val  8021  2nd2val  8022  cnvoprab  8064  fnsuppeq0  8196  ecopovtrn  8839  limensuci  9172  pwfilem  9333  r1sucg  9788  jech9.3  9833  rankbnd2  9888  djuin  9937  compss  10395  zorn2lem4  10518  iunfo  10558  cardf  10569  alephsuc3  10599  fpwwe2lem12  10661  rankcf  10796  halfnq  10995  addclprlem2  11036  mulgt0sr  11124  mul02lem2  11417  mul02  11418  addrid  11420  mvlladdi  11506  mvllmuli  12079  infrenegsup  12230  8th4div3  12466  halfpm6th  12468  nneo  12682  nummac  12758  numadd  12760  numaddc  12761  nummul1c  12762  decbin0  12853  rpsup  13888  resup  13889  om2uzrdg  13979  m1expcl2  14108  facnn  14298  fac0  14299  faclbnd4lem1  14316  4bc3eq4  14351  hasheq0  14386  f1oun2prg  14941  sqrt1  15295  sqrt4  15296  sqrt9  15297  rddif  15364  abs3lemi  15434  sumss2  15747  divcnvshft  15876  geo2sum2  15895  geomulcvg  15897  geoihalfsum  15903  risefall0lem  16047  bpoly2  16078  bpoly3  16079  sin0  16172  efival  16175  ef01bndlem  16207  cos2bnd  16211  sin4lt0  16218  flodddiv4  16439  2prm  16716  unbenlem  16933  dec5dvds  17089  modxai  17093  mod2xi  17094  mod2xnegi  17096  gcdi  17098  numexp2x  17103  decsplit  17107  setsid  17231  mreexexlem3d  17663  oppchom  17732  2oppchomf  17741  isoval  17783  estrres  18156  oppchofcl  18277  oyoncl  18287  mvdco  19431  m1expaddsub  19484  psgn0fv0  19497  oppglsm  19628  dprd2da  20030  ring1  20275  opprsubg  20317  lsppratlem1  21113  pzriprnglem7  21453  zzngim  21518  cnmsgnsubg  21542  psgninv  21547  zrhpsgnmhm  21549  ply1basfvi  22181  coe1tm  22215  ply1coe  22241  comppfsc  23475  kgeni  23480  xkoinjcn  23630  ufprim  23852  metreslem  24306  retopbas  24704  cnfldms  24719  qdensere2  24741  xrsmopn  24757  metdscn2  24802  pcoass  24980  recvs  25102  recvsOLD  25103  zclmncvs  25105  iscmet3lem3  25247  cncms  25312  cnfldcusp  25314  resscdrg  25315  rrxprds  25346  ovoliunnul  25465  uniioombllem4  25544  vitalilem5  25570  mbfres  25602  ismbf3d  25612  i1fima  25636  i1fd  25639  itg2cnlem1  25719  itgss3  25773  ellimc2  25835  limccnp2  25850  cpnres  25896  lhop  25978  plyeq0  26173  plypf1  26174  sinhalfpilem  26429  sincos6thpi  26482  sincos3rdpi  26483  pige3ALT  26486  dfrelog  26531  logi  26553  logimul  26580  logneg2  26581  dvlog  26617  cxpsqrt  26669  ang180lem2  26777  ang180lem3  26778  ang180lem4  26779  quart1  26823  asin1  26861  atan0  26875  atanlogsublem  26882  atan1  26895  log2tlbnd  26912  log2ublem2  26914  log2ub  26916  basellem8  27055  cht2  27139  ppiub  27172  bposlem6  27257  bposlem8  27259  bposlem9  27260  lgsdir2lem3  27295  lgseisenlem1  27343  lgseisenlem2  27344  lgsquadlem1  27348  lgsquadlem2  27349  2lgsoddprmlem2  27377  chebbnd1  27440  negsbdaylem  28019  om2noseqrdg  28255  zseo  28365  istrkg3ld  28445  tgcgr4  28515  motplusg  28526  ax5seglem7  28919  ex-un  30410  ex-sqrt  30440  ipdirilem  30815  ipasslem10  30825  hisubcomi  31090  normlem0  31095  norm3difi  31133  norm3lem  31135  polid2i  31143  chdmj1i  31467  chjjdiri  31510  spansn0  31527  pjoml4i  31573  cmbr3i  31586  qlaxr3i  31622  honpcani  31811  honpncani  31813  lnopunilem1  31996  lnophmlem2  32003  lnfn0i  32028  pjbdlni  32135  pjclem1  32181  pjclem3  32183  pjci  32186  atomli  32368  atabs2i  32388  mddmdin0i  32417  imadifxp  32587  fnresin  32609  ofpreima2  32649  df1stres  32686  df2ndres  32687  nn0disj01  32802  dfdec100  32814  decdiv10  32875  dpmul100  32876  dpmul1000  32878  dpexpp1  32887  dpadd2  32889  dpadd  32890  dpmul  32892  dpmul4  32893  threehalves  32894  xrge0base  33011  xrge00  33012  xrge0mulgnn0  33015  cyc2fv1  33137  cyc3conja  33173  elrgspnlem4  33245  xrge0slmod  33368  opprqusplusg  33509  opprqusmulr  33511  2sqr3nconstr  33820  cos9thpiminplylem1  33821  cos9thpiminplylem5  33825  lmatfvlem  33851  xrge0iifcnv  33969  lmxrge0  33988  cnrrext  34046  qqtopn  34047  esumrnmpt2  34104  esumpfinvallem  34110  unelldsys  34194  ldgenpisyslem1  34199  measunl  34252  mbfmcst  34296  difelcarsg  34347  carsggect  34355  sibfof  34377  eulerpartlemmf  34412  fib2  34439  fib3  34440  fib4  34441  fib5  34442  fib6  34443  0rrv  34488  coinfliprv  34520  ballotlem2  34526  prodfzo03  34640  chtvalz  34666  hgt750lemd  34685  hgt750lem  34688  hgt750lem2  34689  kur14lem6  35238  kur14lem7  35239  cvmlift2lem12  35341  problem5  35696  quad3  35697  divcnvlin  35755  in-ax8  36247  bj-2upln1upl  37047  bj-rest0  37116  relowlssretop  37386  relowlpssretop  37387  1oequni2o  37391  curunc  37631  ptrest  37648  poimirlem16  37665  poimirlem30  37679  mblfinlem2  37687  ovoliunnfl  37691  voliunnfl  37693  itg2addnclem2  37701  ftc1anclem5  37726  ftc1anclem6  37727  sdc  37773  heiborlem3  37842  xrnresex  38429  dvh4dimN  41471  12gcd5e1  42021  60gcd6e6  42022  60gcd7e1  42023  420gcd8e4  42024  lcmeprodgcdi  42025  lcmineqlem23  42069  sq3deccom12  42308  asin1half  42375  acos1half  42376  redvmptabs  42378  readvrec  42380  sn-it1ei  42454  sn-0tie0  42457  sn-inelr  42485  dnnumch1  43043  aomclem6  43058  areaquad  43215  naddov4  43382  unitadd  44194  seff  44308  sblpnf  44309  hashnzfz  44319  lhe4.4ex1a  44328  xrtgcntopre  45485  iccdifioo  45524  itgsin0pilem1  45959  stoweidlem13  46022  stoweidlem26  46035  fourierdlem62  46177  fourierdlem102  46217  fourierdlem114  46229  fourierswlem  46239  fouriersw  46240  sge0tsms  46389  meaiuninc  46490  tworepnotupword  46895  fmtno4prmfac  47566  41prothprm  47613  dfclnbgr4  47818  2zrngasgrp  48201  2zrngmsgrp  48208  tposres3  48836  setc1onsubc  49459  mvlraddi  49615  mvlrmuli  49621  i2linesi  49622