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 1541

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  3eqtr3i  2767  3eqtr3ri  2768  unundi  4128  unundir  4129  inindi  4187  inindir  4188  dfin4  4230  difun1  4251  difabs  4255  notab  4266  dif0  4330  disjdifr  4425  difdifdir  4444  pwundif  4578  tpidm13  4713  intmin2  4930  iunxdif3  5050  univ  5399  iunxpconst  5697  rnresi  6034  rnresv  6159  cnvsn0  6168  resdmres  6190  coi2  6222  coires1  6223  dfdm2  6239  isarep2  6582  resasplit  6704  ssimaex  6919  fnreseql  6993  resfunexg  7161  mpompt  7472  caov31  7587  fvresex  7904  xpexgALT  7925  1st2val  7961  2nd2val  7962  cnvoprab  8004  fnsuppeq0  8134  ecopovtrn  8757  limensuci  9081  pwfilem  9218  r1sucg  9681  jech9.3  9726  rankbnd2  9781  djuin  9830  compss  10286  zorn2lem4  10409  iunfo  10449  cardf  10460  alephsuc3  10491  fpwwe2lem12  10553  rankcf  10688  halfnq  10887  addclprlem2  10928  mulgt0sr  11016  mul02lem2  11310  mul02  11311  addrid  11313  mvlladdi  11399  mvllmuli  11974  infrenegsup  12125  8th4div3  12361  halfpm6th  12363  nneo  12576  nummac  12652  numadd  12654  numaddc  12655  nummul1c  12656  decbin0  12747  rpsup  13786  resup  13787  om2uzrdg  13879  m1expcl2  14008  facnn  14198  fac0  14199  faclbnd4lem1  14216  4bc3eq4  14251  hasheq0  14286  f1oun2prg  14840  sqrt1  15194  sqrt4  15195  sqrt9  15196  rddif  15264  abs3lemi  15334  sumss2  15649  divcnvshft  15778  geo2sum2  15797  geomulcvg  15799  geoihalfsum  15805  risefall0lem  15949  bpoly2  15980  bpoly3  15981  sin0  16074  efival  16077  ef01bndlem  16109  cos2bnd  16113  sin4lt0  16120  flodddiv4  16342  2prm  16619  unbenlem  16836  dec5dvds  16992  modxai  16996  mod2xi  16997  mod2xnegi  16999  gcdi  17001  numexp2x  17006  decsplit  17010  setsid  17134  xrge0base  17528  mreexexlem3d  17569  oppchom  17638  2oppchomf  17647  isoval  17689  estrres  18062  oppchofcl  18183  oyoncl  18193  mvdco  19374  m1expaddsub  19427  psgn0fv0  19440  oppglsm  19571  dprd2da  19973  ring1  20245  opprsubg  20288  lsppratlem1  21102  pzriprnglem7  21442  zzngim  21507  cnmsgnsubg  21532  psgninv  21537  zrhpsgnmhm  21539  ply1basfvi  22181  coe1tm  22215  ply1coe  22242  comppfsc  23476  kgeni  23481  xkoinjcn  23631  ufprim  23853  metreslem  24306  retopbas  24704  cnfldms  24719  qdensere2  24741  xrsmopn  24757  metdscn2  24802  pcoass  24980  recvs  25102  zclmncvs  25104  iscmet3lem3  25246  cncms  25311  cnfldcusp  25313  resscdrg  25314  rrxprds  25345  ovoliunnul  25464  uniioombllem4  25543  vitalilem5  25569  mbfres  25601  ismbf3d  25611  i1fima  25635  i1fd  25638  itg2cnlem1  25718  itgss3  25772  ellimc2  25834  limccnp2  25849  cpnres  25895  lhop  25977  plyeq0  26172  plypf1  26173  sinhalfpilem  26428  sincos6thpi  26481  sincos3rdpi  26482  pige3ALT  26485  dfrelog  26530  logi  26552  logimul  26579  logneg2  26580  dvlog  26616  cxpsqrt  26668  ang180lem2  26776  ang180lem3  26777  ang180lem4  26778  quart1  26822  asin1  26860  atan0  26874  atanlogsublem  26881  atan1  26894  log2tlbnd  26911  log2ublem2  26913  log2ub  26915  basellem8  27054  cht2  27138  ppiub  27171  bposlem6  27256  bposlem8  27258  bposlem9  27259  lgsdir2lem3  27294  lgseisenlem1  27342  lgseisenlem2  27343  lgsquadlem1  27347  lgsquadlem2  27348  2lgsoddprmlem2  27376  chebbnd1  27439  negbdaylem  28052  om2noseqrdg  28300  zseo  28418  bdaypw2n0bndlem  28459  istrkg3ld  28533  tgcgr4  28603  motplusg  28614  ax5seglem7  29008  ex-un  30499  ex-sqrt  30529  ipdirilem  30904  ipasslem10  30914  hisubcomi  31179  normlem0  31184  norm3difi  31222  norm3lem  31224  polid2i  31232  chdmj1i  31556  chjjdiri  31599  spansn0  31616  pjoml4i  31662  cmbr3i  31675  qlaxr3i  31711  honpcani  31900  honpncani  31902  lnopunilem1  32085  lnophmlem2  32092  lnfn0i  32117  pjbdlni  32224  pjclem1  32270  pjclem3  32272  pjci  32275  atomli  32457  atabs2i  32477  mddmdin0i  32506  imadifxp  32676  fnresin  32702  ofpreima2  32744  df1stres  32783  df2ndres  32784  nn0disj01  32899  dfdec100  32911  decdiv10  32977  dpmul100  32978  dpmul1000  32980  dpexpp1  32989  dpadd2  32991  dpadd  32992  dpmul  32994  dpmul4  32995  threehalves  32996  xrge00  33096  xrge0mulgnn0  33097  cyc2fv1  33203  cyc3conja  33239  elrgspnlem4  33327  xrge0slmod  33429  opprqusplusg  33570  opprqusmulr  33572  extvfvcl  33701  2sqr3nconstr  33938  cos9thpiminplylem1  33939  cos9thpiminplylem5  33943  cos9thpinconstrlem2  33947  lmatfvlem  33972  xrge0iifcnv  34090  lmxrge0  34109  cnrrext  34167  qqtopn  34168  esumrnmpt2  34225  esumpfinvallem  34231  unelldsys  34315  ldgenpisyslem1  34320  measunl  34373  mbfmcst  34416  difelcarsg  34467  carsggect  34475  sibfof  34497  eulerpartlemmf  34532  fib2  34559  fib3  34560  fib4  34561  fib5  34562  fib6  34563  0rrv  34608  coinfliprv  34640  ballotlem2  34646  prodfzo03  34760  chtvalz  34786  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  kur14lem6  35405  kur14lem7  35406  cvmlift2lem12  35508  problem5  35863  quad3  35864  divcnvlin  35927  in-ax8  36418  bj-2upln1upl  37225  bj-rest0  37298  relowlssretop  37568  relowlpssretop  37569  1oequni2o  37573  curunc  37803  ptrest  37820  poimirlem16  37837  poimirlem30  37851  mblfinlem2  37859  ovoliunnfl  37863  voliunnfl  37865  itg2addnclem2  37873  ftc1anclem5  37898  ftc1anclem6  37899  sdc  37945  heiborlem3  38014  xrnresex  38614  dmxrncnvepres  38617  dvh4dimN  41707  12gcd5e1  42257  60gcd6e6  42258  60gcd7e1  42259  420gcd8e4  42260  lcmeprodgcdi  42261  lcmineqlem23  42305  sq3deccom12  42545  asin1half  42612  acos1half  42613  redvmptabs  42615  readvrec  42617  sn-it1ei  42692  sn-0tie0  42706  dnnumch1  43286  aomclem6  43301  areaquad  43458  naddov4  43625  unitadd  44436  seff  44550  sblpnf  44551  hashnzfz  44561  lhe4.4ex1a  44570  xrtgcntopre  45722  iccdifioo  45761  itgsin0pilem1  46194  stoweidlem13  46257  stoweidlem26  46270  fourierdlem62  46412  fourierdlem102  46452  fourierdlem114  46464  fourierswlem  46474  fouriersw  46475  sge0tsms  46624  meaiuninc  46725  fmtno4prmfac  47818  41prothprm  47865  dfclnbgr4  48070  2zrngasgrp  48492  2zrngmsgrp  48499  tposres3  49126  eloppf  49378  setc1onsubc  49847  mvlraddi  50016  mvlrmuli  50022  i2linesi  50023