Theorem eqtr3i 2787

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  3eqtr3i  2793  3eqtr3ri  2794  unundi  4128  unundir  4129  inindi  4186  inindir  4187  dfin4  4230  difun1  4251  difabs  4255  notab  4266  dif0  4331  difdifdir  4445  pwundif  4580  tpidm13  4715  intmin2  4933  iunxdif3  5052  univ  5418  iunxpconst  5720  resdmdfsn  6018  rnresi  6064  rnresv  6188  cnvsn0  6197  resdmres  6219  coi2  6251  coires1  6252  dfdm2  6268  isarep2  6611  resasplit  6734  ssimaex  6952  fnreseql  7029  resfunexg  7199  mpompt  7510  caov31  7625  fvresex  7941  xpexgALT  7962  1st2val  7998  2nd2val  7999  cnvoprab  8041  fnsuppeq0  8172  ecopovtrn  8802  limensuci  9125  pwfilem  9262  r1sucg  9727  jech9.3  9772  rankbnd2  9827  djuin  9876  compss  10333  zorn2lem4  10456  iunfo  10496  cardf  10507  alephsuc3  10538  fpwwe2lem12  10600  rankcf  10735  halfnq  10934  addclprlem2  10975  mulgt0sr  11063  mul02lem2  11360  mul02  11361  addrid  11363  mvlladdi  11449  mvllmuli  12024  infrenegsup  12175  8th4div3  12441  halfpm6th  12443  nneo  12657  nummac  12738  numadd  12740  numaddc  12741  nummul1c  12742  decbin0  12835  rpsup  13876  resup  13877  om2uzrdg  13969  m1expcl2  14098  facnn  14288  fac0  14289  faclbnd4lem1  14306  4bc3eq4  14341  hasheq0  14376  f1oun2prg  14930  sqrt1  15298  sqrt4  15299  sqrt9  15300  rddif  15368  abs3lemi  15438  sumss2  15753  divcnvshft  15885  geo2sum2  15904  geomulcvg  15906  geoihalfsum  15912  risefall0lem  16056  bpoly2  16087  bpoly3  16088  sin0  16181  efival  16184  ef01bndlem  16216  cos2bnd  16220  sin4lt0  16227  flodddiv4  16449  2prm  16726  unbenlem  16944  dec5dvds  17100  modxai  17104  mod2xi  17105  mod2xnegi  17107  gcdi  17109  numexp2x  17114  decsplit  17118  setsid  17243  xrge0base  17637  mreexexlem3d  17678  oppchom  17747  2oppchomf  17756  isoval  17798  estrres  18171  oppchofcl  18292  oyoncl  18302  mvdco  19485  m1expaddsub  19538  psgn0fv0  19551  oppglsm  19682  dprd2da  20084  ring1  20356  opprsubg  20397  lsppratlem1  21214  pzriprnglem7  21536  zzngim  21601  cnmsgnsubg  21626  psgninv  21631  zrhpsgnmhm  21633  ply1basfvi  22299  coe1tm  22333  ply1coe  22358  comppfsc  23589  kgeni  23594  xkoinjcn  23744  ufprim  23966  metreslem  24419  retopbas  24817  cnfldms  24832  qdensere2  24854  xrsmopn  24870  metdscn2  24915  pcoass  25083  recvs  25205  zclmncvs  25207  iscmet3lem3  25349  cncms  25414  cnfldcusp  25416  resscdrg  25417  rrxprds  25448  ovoliunnul  25566  uniioombllem4  25645  vitalilem5  25671  mbfres  25703  ismbf3d  25713  i1fima  25737  i1fd  25740  itg2cnlem1  25820  itgss3  25874  ellimc2  25936  limccnp2  25951  cpnres  25996  lhop  26075  plyeq0  26268  plypf1  26269  sinhalfpilem  26525  sincos6thpi  26578  sincos3rdpi  26579  pige3ALT  26582  dfrelog  26627  logi  26649  logimul  26676  logneg2  26677  dvlog  26713  cxpsqrt  26765  ang180lem2  26872  ang180lem3  26873  ang180lem4  26874  quart1  26918  asin1  26956  atan0  26970  atanlogsublem  26977  atan1  26990  log2tlbnd  27007  log2ublem2  27009  log2ub  27011  basellem8  27149  cht2  27233  ppiub  27265  bposlem6  27350  bposlem8  27352  bposlem9  27353  lgsdir2lem3  27388  lgseisenlem1  27436  lgseisenlem2  27437  lgsquadlem1  27441  lgsquadlem2  27442  2lgsoddprmlem2  27470  chebbnd1  27533  negbdaylem  28146  om2noseqrdg  28394  zseo  28512  bdaypw2n0bndlem  28553  istrkg3ld  28627  tgcgr4  28697  motplusg  28708  ax5seglem7  29133  ex-un  30623  ex-sqrt  30653  ipdirilem  31029  ipasslem10  31039  hisubcomi  31304  normlem0  31309  norm3difi  31347  norm3lem  31349  polid2i  31357  chdmj1i  31681  chjjdiri  31724  spansn0  31741  pjoml4i  31787  cmbr3i  31800  qlaxr3i  31836  honpcani  32025  honpncani  32027  lnopunilem1  32210  lnophmlem2  32217  lnfn0i  32242  pjbdlni  32349  pjclem1  32395  pjclem3  32397  pjci  32400  atomli  32582  atabs2i  32602  mddmdin0i  32631  imadifxp  32798  fnresin  32823  ofpreima2  32865  df1stres  32903  df2ndres  32904  nn0disj01  33018  dfdec100  33029  decdiv10  33070  dpmul100  33071  dpmul1000  33073  dpexpp1  33082  dpadd2  33084  dpadd  33085  dpmul  33087  dpmul4  33088  threehalves  33089  xrge00  33189  xrge0mulgnn0  33190  cyc2fv1  33298  cyc3conja  33334  elrgspnlem4  33423  xrge0slmod  33531  opprqusplusg  33674  opprqusmulr  33676  selvply1rhmlemb  33813  extvfvcl  33830  2sqr3nconstr  34075  cos9thpiminplylem1  34076  cos9thpiminplylem5  34080  cos9thpinconstrlem2  34084  lmatfvlem  34109  xrge0iifcnv  34227  lmxrge0  34246  cnrrext  34304  qqtopn  34305  esumrnmpt2  34362  esumpfinvallem  34368  unelldsys  34452  ldgenpisyslem1  34457  measunl  34510  mbfmcst  34553  difelcarsg  34604  carsggect  34612  sibfof  34634  eulerpartlemmf  34669  fib2  34696  fib3  34697  fib4  34698  fib5  34699  fib6  34700  0rrv  34745  coinfliprv  34777  ballotlem2  34783  prodfzo03  34894  chtvalz  34920  hgt750lemd  34939  hgt750lem  34942  hgt750lem2  34943  kur14lem6  35558  kur14lem7  35559  cvmlift2lem12  35661  problem5  36016  quad3  36017  divcnvlin  36080  in-ax8  36581  bj-2upln1upl  37506  bj-rest0  37580  relowlssretop  37854  relowlpssretop  37855  1oequni2o  37859  curunc  38098  ptrest  38115  poimirlem16  38132  poimirlem30  38146  mblfinlem2  38154  ovoliunnfl  38158  voliunnfl  38160  itg2addnclem2  38168  ftc1anclem5  38193  ftc1anclem6  38194  sdc  38240  heiborlem3  38309  xrnresex  38925  dmxrncnvepres  38928  dvh4dimN  42068  12gcd5e1  42617  60gcd6e6  42618  60gcd7e1  42619  420gcd8e4  42620  lcmeprodgcdi  42621  lcmineqlem23  42665  sq3deccom12  42896  asin1half  42963  acos1half  42964  redvmptabs  42966  readvrec  42968  sn-it1ei  43043  sn-0tie0  43070  dnnumch1  43618  aomclem6  43633  areaquad  43790  naddov4  43957  unitadd  44768  seff  44882  sblpnf  44883  hashnzfz  44893  lhe4.4ex1a  44902  xrtgcntopre  46049  iccdifioo  46088  itgsin0pilem1  46521  stoweidlem13  46584  stoweidlem26  46597  fourierdlem62  46739  fourierdlem102  46779  fourierdlem114  46791  fourierswlem  46801  fouriersw  46802  sge0tsms  46951  meaiuninc  47052  cos5t  47470  fmtno4prmfac  48178  41prothprm  48225  ppivalnn4  48233  dfclnbgr4  48443  2zrngasgrp  48865  2zrngmsgrp  48872  tposres3  49499  eloppf  49751  setc1onsubc  50220  mvlraddi  50389  mvlrmuli  50395  i2linesi  50396