Theorem eqtr3i 2805

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

Syntax hints:   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2772

This theorem is referenced by:  3eqtr3i  2811  3eqtr3ri  2812  rabrabi  3415  unundi  4036  unundir  4037  inindi  4091  inindir  4092  dfin4  4132  difun1  4152  difabs  4156  notab  4161  dif0  4219  difdifdir  4320  tpidm13  4566  intmin2  4776  iunxdif3  4883  univ  5200  iunxpconst  5474  opabresid  5761  rnresi  5783  rnresv  5897  cnvsn0  5906  resdmres  5928  coi2  5955  coires1  5956  dfdm2  5970  isarep2  6276  resasplit  6377  ssimaex  6576  fnreseql  6643  idref  6731  resfunexg  6804  mpompt  7082  caov31  7193  fvresex  7473  xpexgALT  7494  1st2val  7529  2nd2val  7530  cnvoprab  7566  fnsuppeq0  7661  ecopovtrn  8200  limensuci  8489  pssnn  8531  r1sucg  8992  jech9.3  9037  rankbnd2  9092  djuin  9141  compss  9596  zorn2lem4  9719  iunfo  9759  cardf  9770  alephsuc3  9800  fpwwe2lem13  9862  rankcf  9997  halfnq  10196  addclprlem2  10237  mulgt0sr  10325  mul02lem2  10617  mul02  10618  addid1  10620  mvlladdi  10705  mvllmuli  11274  infrenegsup  11425  8th4div3  11667  nneo  11879  nummac  11957  numadd  11959  numaddc  11960  nummul1c  11961  decbin0  12053  rpsup  13049  resup  13050  om2uzrdg  13139  m1expcl2  13266  facnn  13450  fac0  13451  faclbnd4lem1  13468  4bc3eq4  13503  hasheq0  13539  f1oun2prg  14141  sqrt1  14492  sqrt4  14493  sqrt9  14494  rddif  14561  abs3lemi  14631  sumss2  14943  divcnvshft  15070  geo2sum2  15090  geomulcvg  15092  geoihalfsum  15098  risefall0lem  15240  bpoly2  15271  bpoly3  15272  sin0  15362  efival  15365  ef01bndlem  15397  cos2bnd  15401  sin4lt0  15408  flodddiv4  15624  2prm  15892  unbenlem  16100  dec5dvds  16256  modxai  16260  mod2xi  16261  mod2xnegi  16263  gcdi  16265  numexp2x  16271  decsplit  16275  setsid  16394  mreexexlem3d  16775  oppchom  16843  2oppchomf  16852  isoval  16893  estrres  17247  oppchofcl  17368  oyoncl  17378  mvdco  18334  m1expaddsub  18388  psgn0fv0  18401  oppglsm  18528  dprd2da  18914  ring1  19075  opprsubg  19109  lsppratlem1  19641  opsrtoslem1  19977  ply1basfvi  20112  coe1tm  20144  ply1coe  20167  zzngim  20401  cnmsgnsubg  20423  psgninv  20428  zrhpsgnmhm  20430  neitr  21492  comppfsc  21844  kgeni  21849  xkoinjcn  21999  ufprim  22221  metreslem  22675  restmetu  22883  retopbas  23072  cnfldms  23087  qdensere2  23108  xrsmopn  23123  metdscn2  23168  pcoass  23331  recvs  23453  zclmncvs  23455  iscmet3lem3  23596  cncms  23661  cnfldcusp  23663  resscdrg  23664  rrxprds  23695  ovoliunnul  23811  uniioombllem4  23890  vitalilem5  23916  mbfres  23948  ismbf3d  23958  i1fima  23982  i1fd  23985  itg2cnlem1  24065  itgss3  24118  ellimc2  24178  limccnp2  24193  cpnres  24237  lhop  24316  plyeq0  24504  plypf1  24505  sinhalfpilem  24752  sincos6thpi  24804  sincos3rdpi  24805  pige3ALT  24808  dfrelog  24850  logimul  24898  logneg2  24899  dvlog  24935  cxpsqrt  24987  ang180lem2  25089  ang180lem3  25090  ang180lem4  25091  quart1  25135  asin1  25173  atan0  25187  atanlogsublem  25194  atan1  25207  log2tlbnd  25225  log2ublem2  25227  log2ub  25229  basellem8  25367  cht2  25451  ppiub  25482  bposlem6  25567  bposlem8  25569  bposlem9  25570  lgsdir2lem3  25605  lgseisenlem1  25653  lgseisenlem2  25654  lgsquadlem1  25658  lgsquadlem2  25659  2lgsoddprmlem2  25687  chebbnd1  25750  istrkg3ld  25949  tgcgr4  26019  motplusg  26030  ax5seglem7  26424  ex-un  27981  ex-sqrt  28011  ipdirilem  28383  ipasslem10  28393  hisubcomi  28660  normlem0  28665  norm3difi  28703  norm3lem  28705  polid2i  28713  chdmj1i  29039  chjjdiri  29082  spansn0  29099  pjoml4i  29145  cmbr3i  29158  qlaxr3i  29194  honpcani  29383  honpncani  29385  lnopunilem1  29568  lnophmlem2  29575  lnfn0i  29600  pjbdlni  29707  pjclem1  29753  pjclem3  29755  pjci  29758  atomli  29940  atabs2i  29960  mddmdin0i  29989  difeq  30056  disjdifprg  30091  imadifxp  30117  fnresin  30135  ofpreima2  30173  df1stres  30191  df2ndres  30192  cnvoprabOLD  30208  dfdec100  30292  decdiv10  30318  dpmul100  30319  dpmul1000  30321  dpexpp1  30330  dpadd2  30332  dpadd  30333  dpmul  30335  dpmul4  30336  threehalves  30337  xrge0base  30401  xrge00  30402  xrge0mulgnn0  30405  cycpmfv1  30444  cycpmfv2  30445  cycpmfv3  30446  cycpmcl  30447  cyc2fv1  30450  xrge0slmod  30593  lmatfvlem  30719  xrge0iifcnv  30817  lmxrge0  30836  cnrrext  30892  qqtopn  30893  esumrnmpt2  30968  esumpfinvallem  30974  unelldsys  31059  ldgenpisyslem1  31064  measunl  31117  mbfmcst  31159  difelcarsg  31210  carsggect  31218  sibfof  31240  eulerpartlemmf  31275  fib2  31303  fib3  31304  fib4  31305  fib5  31306  fib6  31307  0rrv  31352  coinfliprv  31383  ballotlem2  31389  prodfzo03  31519  chtvalz  31545  hgt750lemd  31564  hgt750lem  31567  hgt750lem2  31568  kur14lem6  32040  kur14lem7  32041  cvmlift2lem12  32143  problem5  32429  quad3  32430  divcnvlin  32481  logi  32483  bj-2upln1upl  33851  bj-rest0  33891  relowlssretop  34083  relowlpssretop  34084  1oequni2o  34088  curunc  34312  ptrest  34329  poimirlem16  34346  poimirlem30  34360  mblfinlem2  34368  ovoliunnfl  34372  voliunnfl  34374  itg2addnclem2  34382  ftc1anclem5  34409  ftc1anclem6  34410  sdc  34458  heiborlem3  34530  xrnresex  35096  dvh4dimN  38025  sq3deccom12  38605  dnnumch1  39037  aomclem6  39052  areaquad  39216  unitadd  39910  seff  40054  sblpnf  40055  hashnzfz  40065  lhe4.4ex1a  40074  xrtgcntopre  41184  iccdifioo  41220  itgsin0pilem1  41663  stoweidlem13  41727  stoweidlem26  41740  fourierdlem62  41882  fourierdlem102  41922  fourierdlem114  41934  fourierswlem  41944  fouriersw  41945  sge0tsms  42091  meaiuninc  42192  fmtno4prmfac  43100  41prothprm  43150  2zrngasgrp  43573  2zrngmsgrp  43580  mvlraddi  44236  mvlrmuli  44243  i2linesi  44244