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  4117  unundir  4118  inindi  4176  inindir  4177  dfin4  4219  difun1  4240  difabs  4244  notab  4255  dif0  4319  difdifdir  4432  pwundif  4566  tpidm13  4701  intmin2  4918  iunxdif3  5038  univ  5399  iunxpconst  5698  rnresi  6035  rnresv  6160  cnvsn0  6169  resdmres  6191  coi2  6223  coires1  6224  dfdm2  6240  isarep2  6583  resasplit  6705  ssimaex  6920  fnreseql  6995  resfunexg  7164  mpompt  7475  caov31  7590  fvresex  7907  xpexgALT  7928  1st2val  7964  2nd2val  7965  cnvoprab  8007  fnsuppeq0  8136  ecopovtrn  8761  limensuci  9085  pwfilem  9222  r1sucg  9687  jech9.3  9732  rankbnd2  9787  djuin  9836  compss  10292  zorn2lem4  10415  iunfo  10455  cardf  10466  alephsuc3  10497  fpwwe2lem12  10559  rankcf  10694  halfnq  10893  addclprlem2  10934  mulgt0sr  11022  mul02lem2  11317  mul02  11318  addrid  11320  mvlladdi  11406  mvllmuli  11982  infrenegsup  12133  8th4div3  12391  halfpm6th  12393  nneo  12607  nummac  12683  numadd  12685  numaddc  12686  nummul1c  12687  decbin0  12778  rpsup  13819  resup  13820  om2uzrdg  13912  m1expcl2  14041  facnn  14231  fac0  14232  faclbnd4lem1  14249  4bc3eq4  14284  hasheq0  14319  f1oun2prg  14873  sqrt1  15227  sqrt4  15228  sqrt9  15229  rddif  15297  abs3lemi  15367  sumss2  15682  divcnvshft  15814  geo2sum2  15833  geomulcvg  15835  geoihalfsum  15841  risefall0lem  15985  bpoly2  16016  bpoly3  16017  sin0  16110  efival  16113  ef01bndlem  16145  cos2bnd  16149  sin4lt0  16156  flodddiv4  16378  2prm  16655  unbenlem  16873  dec5dvds  17029  modxai  17033  mod2xi  17034  mod2xnegi  17036  gcdi  17038  numexp2x  17043  decsplit  17047  setsid  17171  xrge0base  17565  mreexexlem3d  17606  oppchom  17675  2oppchomf  17684  isoval  17726  estrres  18099  oppchofcl  18220  oyoncl  18230  mvdco  19414  m1expaddsub  19467  psgn0fv0  19480  oppglsm  19611  dprd2da  20013  ring1  20285  opprsubg  20326  lsppratlem1  21140  pzriprnglem7  21480  zzngim  21545  cnmsgnsubg  21570  psgninv  21575  zrhpsgnmhm  21577  ply1basfvi  22217  coe1tm  22251  ply1coe  22276  comppfsc  23510  kgeni  23515  xkoinjcn  23665  ufprim  23887  metreslem  24340  retopbas  24738  cnfldms  24753  qdensere2  24775  xrsmopn  24791  metdscn2  24836  pcoass  25004  recvs  25126  zclmncvs  25128  iscmet3lem3  25270  cncms  25335  cnfldcusp  25337  resscdrg  25338  rrxprds  25369  ovoliunnul  25487  uniioombllem4  25566  vitalilem5  25592  mbfres  25624  ismbf3d  25634  i1fima  25658  i1fd  25661  itg2cnlem1  25741  itgss3  25795  ellimc2  25857  limccnp2  25872  cpnres  25917  lhop  25996  plyeq0  26189  plypf1  26190  sinhalfpilem  26443  sincos6thpi  26496  sincos3rdpi  26497  pige3ALT  26500  dfrelog  26545  logi  26567  logimul  26594  logneg2  26595  dvlog  26631  cxpsqrt  26683  ang180lem2  26790  ang180lem3  26791  ang180lem4  26792  quart1  26836  asin1  26874  atan0  26888  atanlogsublem  26895  atan1  26908  log2tlbnd  26925  log2ublem2  26927  log2ub  26929  basellem8  27068  cht2  27152  ppiub  27184  bposlem6  27269  bposlem8  27271  bposlem9  27272  lgsdir2lem3  27307  lgseisenlem1  27355  lgseisenlem2  27356  lgsquadlem1  27360  lgsquadlem2  27361  2lgsoddprmlem2  27389  chebbnd1  27452  negbdaylem  28065  om2noseqrdg  28313  zseo  28431  bdaypw2n0bndlem  28472  istrkg3ld  28546  tgcgr4  28616  motplusg  28627  ax5seglem7  29021  ex-un  30512  ex-sqrt  30542  ipdirilem  30918  ipasslem10  30928  hisubcomi  31193  normlem0  31198  norm3difi  31236  norm3lem  31238  polid2i  31246  chdmj1i  31570  chjjdiri  31613  spansn0  31630  pjoml4i  31676  cmbr3i  31689  qlaxr3i  31725  honpcani  31914  honpncani  31916  lnopunilem1  32099  lnophmlem2  32106  lnfn0i  32131  pjbdlni  32238  pjclem1  32284  pjclem3  32286  pjci  32289  atomli  32471  atabs2i  32491  mddmdin0i  32520  imadifxp  32689  fnresin  32715  ofpreima2  32757  df1stres  32795  df2ndres  32796  nn0disj01  32910  dfdec100  32921  decdiv10  32973  dpmul100  32974  dpmul1000  32976  dpexpp1  32985  dpadd2  32987  dpadd  32988  dpmul  32990  dpmul4  32991  threehalves  32992  xrge00  33092  xrge0mulgnn0  33093  cyc2fv1  33200  cyc3conja  33236  elrgspnlem4  33324  xrge0slmod  33426  opprqusplusg  33567  opprqusmulr  33569  extvfvcl  33698  2sqr3nconstr  33944  cos9thpiminplylem1  33945  cos9thpiminplylem5  33949  cos9thpinconstrlem2  33953  lmatfvlem  33978  xrge0iifcnv  34096  lmxrge0  34115  cnrrext  34173  qqtopn  34174  esumrnmpt2  34231  esumpfinvallem  34237  unelldsys  34321  ldgenpisyslem1  34326  measunl  34379  mbfmcst  34422  difelcarsg  34473  carsggect  34481  sibfof  34503  eulerpartlemmf  34538  fib2  34565  fib3  34566  fib4  34567  fib5  34568  fib6  34569  0rrv  34614  coinfliprv  34646  ballotlem2  34652  prodfzo03  34766  chtvalz  34792  hgt750lemd  34811  hgt750lem  34814  hgt750lem2  34815  kur14lem6  35412  kur14lem7  35413  cvmlift2lem12  35515  problem5  35870  quad3  35871  divcnvlin  35934  in-ax8  36425  bj-2upln1upl  37350  bj-rest0  37424  relowlssretop  37696  relowlpssretop  37697  1oequni2o  37701  curunc  37940  ptrest  37957  poimirlem16  37974  poimirlem30  37988  mblfinlem2  37996  ovoliunnfl  38000  voliunnfl  38002  itg2addnclem2  38010  ftc1anclem5  38035  ftc1anclem6  38036  sdc  38082  heiborlem3  38151  xrnresex  38767  dmxrncnvepres  38770  dvh4dimN  41910  12gcd5e1  42459  60gcd6e6  42460  60gcd7e1  42461  420gcd8e4  42462  lcmeprodgcdi  42463  lcmineqlem23  42507  sq3deccom12  42739  asin1half  42806  acos1half  42807  redvmptabs  42809  readvrec  42811  sn-it1ei  42886  sn-0tie0  42913  dnnumch1  43493  aomclem6  43508  areaquad  43665  naddov4  43832  unitadd  44643  seff  44757  sblpnf  44758  hashnzfz  44768  lhe4.4ex1a  44777  xrtgcntopre  45927  iccdifioo  45966  itgsin0pilem1  46399  stoweidlem13  46462  stoweidlem26  46475  fourierdlem62  46617  fourierdlem102  46657  fourierdlem114  46669  fourierswlem  46679  fouriersw  46680  sge0tsms  46829  meaiuninc  46930  fmtno4prmfac  48050  41prothprm  48097  ppivalnn4  48105  dfclnbgr4  48315  2zrngasgrp  48737  2zrngmsgrp  48744  tposres3  49371  eloppf  49623  setc1onsubc  50092  mvlraddi  50261  mvlrmuli  50267  i2linesi  50268