Theorem eqtr3i 2762

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

Syntax hints:   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtr3i  2768  3eqtr3ri  2769  unundi  4130  unundir  4131  inindi  4189  inindir  4190  dfin4  4232  difun1  4253  difabs  4257  notab  4268  dif0  4332  disjdifr  4427  difdifdir  4446  pwundif  4580  tpidm13  4715  intmin2  4932  iunxdif3  5052  univ  5406  iunxpconst  5705  rnresi  6042  rnresv  6167  cnvsn0  6176  resdmres  6198  coi2  6230  coires1  6231  dfdm2  6247  isarep2  6590  resasplit  6712  ssimaex  6927  fnreseql  7002  resfunexg  7171  mpompt  7482  caov31  7597  fvresex  7914  xpexgALT  7935  1st2val  7971  2nd2val  7972  cnvoprab  8014  fnsuppeq0  8144  ecopovtrn  8769  limensuci  9093  pwfilem  9230  r1sucg  9693  jech9.3  9738  rankbnd2  9793  djuin  9842  compss  10298  zorn2lem4  10421  iunfo  10461  cardf  10472  alephsuc3  10503  fpwwe2lem12  10565  rankcf  10700  halfnq  10899  addclprlem2  10940  mulgt0sr  11028  mul02lem2  11322  mul02  11323  addrid  11325  mvlladdi  11411  mvllmuli  11986  infrenegsup  12137  8th4div3  12373  halfpm6th  12375  nneo  12588  nummac  12664  numadd  12666  numaddc  12667  nummul1c  12668  decbin0  12759  rpsup  13798  resup  13799  om2uzrdg  13891  m1expcl2  14020  facnn  14210  fac0  14211  faclbnd4lem1  14228  4bc3eq4  14263  hasheq0  14298  f1oun2prg  14852  sqrt1  15206  sqrt4  15207  sqrt9  15208  rddif  15276  abs3lemi  15346  sumss2  15661  divcnvshft  15790  geo2sum2  15809  geomulcvg  15811  geoihalfsum  15817  risefall0lem  15961  bpoly2  15992  bpoly3  15993  sin0  16086  efival  16089  ef01bndlem  16121  cos2bnd  16125  sin4lt0  16132  flodddiv4  16354  2prm  16631  unbenlem  16848  dec5dvds  17004  modxai  17008  mod2xi  17009  mod2xnegi  17011  gcdi  17013  numexp2x  17018  decsplit  17022  setsid  17146  xrge0base  17540  mreexexlem3d  17581  oppchom  17650  2oppchomf  17659  isoval  17701  estrres  18074  oppchofcl  18195  oyoncl  18205  mvdco  19386  m1expaddsub  19439  psgn0fv0  19452  oppglsm  19583  dprd2da  19985  ring1  20257  opprsubg  20300  lsppratlem1  21114  pzriprnglem7  21454  zzngim  21519  cnmsgnsubg  21544  psgninv  21549  zrhpsgnmhm  21551  ply1basfvi  22193  coe1tm  22227  ply1coe  22254  comppfsc  23488  kgeni  23493  xkoinjcn  23643  ufprim  23865  metreslem  24318  retopbas  24716  cnfldms  24731  qdensere2  24753  xrsmopn  24769  metdscn2  24814  pcoass  24992  recvs  25114  zclmncvs  25116  iscmet3lem3  25258  cncms  25323  cnfldcusp  25325  resscdrg  25326  rrxprds  25357  ovoliunnul  25476  uniioombllem4  25555  vitalilem5  25581  mbfres  25613  ismbf3d  25623  i1fima  25647  i1fd  25650  itg2cnlem1  25730  itgss3  25784  ellimc2  25846  limccnp2  25861  cpnres  25907  lhop  25989  plyeq0  26184  plypf1  26185  sinhalfpilem  26440  sincos6thpi  26493  sincos3rdpi  26494  pige3ALT  26497  dfrelog  26542  logi  26564  logimul  26591  logneg2  26592  dvlog  26628  cxpsqrt  26680  ang180lem2  26788  ang180lem3  26789  ang180lem4  26790  quart1  26834  asin1  26872  atan0  26886  atanlogsublem  26893  atan1  26906  log2tlbnd  26923  log2ublem2  26925  log2ub  26927  basellem8  27066  cht2  27150  ppiub  27183  bposlem6  27268  bposlem8  27270  bposlem9  27271  lgsdir2lem3  27306  lgseisenlem1  27354  lgseisenlem2  27355  lgsquadlem1  27359  lgsquadlem2  27360  2lgsoddprmlem2  27388  chebbnd1  27451  negbdaylem  28064  om2noseqrdg  28312  zseo  28430  bdaypw2n0bndlem  28471  istrkg3ld  28545  tgcgr4  28615  motplusg  28626  ax5seglem7  29020  ex-un  30511  ex-sqrt  30541  ipdirilem  30917  ipasslem10  30927  hisubcomi  31192  normlem0  31197  norm3difi  31235  norm3lem  31237  polid2i  31245  chdmj1i  31569  chjjdiri  31612  spansn0  31629  pjoml4i  31675  cmbr3i  31688  qlaxr3i  31724  honpcani  31913  honpncani  31915  lnopunilem1  32098  lnophmlem2  32105  lnfn0i  32130  pjbdlni  32237  pjclem1  32283  pjclem3  32285  pjci  32288  atomli  32470  atabs2i  32490  mddmdin0i  32519  imadifxp  32688  fnresin  32714  ofpreima2  32756  df1stres  32794  df2ndres  32795  nn0disj01  32910  dfdec100  32922  decdiv10  32988  dpmul100  32989  dpmul1000  32991  dpexpp1  33000  dpadd2  33002  dpadd  33003  dpmul  33005  dpmul4  33006  threehalves  33007  xrge00  33107  xrge0mulgnn0  33108  cyc2fv1  33215  cyc3conja  33251  elrgspnlem4  33339  xrge0slmod  33441  opprqusplusg  33582  opprqusmulr  33584  extvfvcl  33713  2sqr3nconstr  33959  cos9thpiminplylem1  33960  cos9thpiminplylem5  33964  cos9thpinconstrlem2  33968  lmatfvlem  33993  xrge0iifcnv  34111  lmxrge0  34130  cnrrext  34188  qqtopn  34189  esumrnmpt2  34246  esumpfinvallem  34252  unelldsys  34336  ldgenpisyslem1  34341  measunl  34394  mbfmcst  34437  difelcarsg  34488  carsggect  34496  sibfof  34518  eulerpartlemmf  34553  fib2  34580  fib3  34581  fib4  34582  fib5  34583  fib6  34584  0rrv  34629  coinfliprv  34661  ballotlem2  34667  prodfzo03  34781  chtvalz  34807  hgt750lemd  34826  hgt750lem  34829  hgt750lem2  34830  kur14lem6  35427  kur14lem7  35428  cvmlift2lem12  35530  problem5  35885  quad3  35886  divcnvlin  35949  in-ax8  36440  bj-2upln1upl  37272  bj-rest0  37346  relowlssretop  37618  relowlpssretop  37619  1oequni2o  37623  curunc  37853  ptrest  37870  poimirlem16  37887  poimirlem30  37901  mblfinlem2  37909  ovoliunnfl  37913  voliunnfl  37915  itg2addnclem2  37923  ftc1anclem5  37948  ftc1anclem6  37949  sdc  37995  heiborlem3  38064  xrnresex  38680  dmxrncnvepres  38683  dvh4dimN  41823  12gcd5e1  42373  60gcd6e6  42374  60gcd7e1  42375  420gcd8e4  42376  lcmeprodgcdi  42377  lcmineqlem23  42421  sq3deccom12  42660  asin1half  42727  acos1half  42728  redvmptabs  42730  readvrec  42732  sn-it1ei  42807  sn-0tie0  42821  dnnumch1  43401  aomclem6  43416  areaquad  43573  naddov4  43740  unitadd  44551  seff  44665  sblpnf  44666  hashnzfz  44676  lhe4.4ex1a  44685  xrtgcntopre  45836  iccdifioo  45875  itgsin0pilem1  46308  stoweidlem13  46371  stoweidlem26  46384  fourierdlem62  46526  fourierdlem102  46566  fourierdlem114  46578  fourierswlem  46588  fouriersw  46589  sge0tsms  46738  meaiuninc  46839  fmtno4prmfac  47932  41prothprm  47979  dfclnbgr4  48184  2zrngasgrp  48606  2zrngmsgrp  48613  tposres3  49240  eloppf  49492  setc1onsubc  49961  mvlraddi  50130  mvlrmuli  50136  i2linesi  50137