Theorem eqtr3i 2823

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

Syntax hints:   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  3eqtr3i  2829  3eqtr3ri  2830  rabrabi  3440  unundi  4097  unundir  4098  inindi  4153  inindir  4154  dfin4  4194  difun1  4214  difabs  4218  notab  4225  dif0  4286  difdifdir  4395  pwundif  4523  tpidm13  4652  intmin2  4865  iunxdif3  4980  univ  5309  iunxpconst  5588  opabresidOLD  5886  rnresi  5910  rnresv  6025  cnvsn0  6034  resdmres  6056  coi2  6083  coires1  6084  dfdm2  6100  isarep2  6413  resasplit  6522  ssimaex  6723  fnreseql  6795  resfunexg  6955  mpompt  7245  caov31  7357  fvresex  7643  xpexgALT  7664  1st2val  7699  2nd2val  7700  cnvoprab  7740  fnsuppeq0  7841  ecopovtrn  8383  limensuci  8677  pssnn  8720  r1sucg  9182  jech9.3  9227  rankbnd2  9282  djuin  9331  compss  9787  zorn2lem4  9910  iunfo  9950  cardf  9961  alephsuc3  9991  fpwwe2lem13  10053  rankcf  10188  halfnq  10387  addclprlem2  10428  mulgt0sr  10516  mul02lem2  10806  mul02  10807  addid1  10809  mvlladdi  10893  mvllmuli  11462  infrenegsup  11611  8th4div3  11845  nneo  12054  nummac  12131  numadd  12133  numaddc  12134  nummul1c  12135  decbin0  12226  rpsup  13229  resup  13230  om2uzrdg  13319  m1expcl2  13447  facnn  13631  fac0  13632  faclbnd4lem1  13649  4bc3eq4  13684  hasheq0  13720  f1oun2prg  14270  sqrt1  14623  sqrt4  14624  sqrt9  14625  rddif  14692  abs3lemi  14762  sumss2  15075  divcnvshft  15202  geo2sum2  15222  geomulcvg  15224  geoihalfsum  15230  risefall0lem  15372  bpoly2  15403  bpoly3  15404  sin0  15494  efival  15497  ef01bndlem  15529  cos2bnd  15533  sin4lt0  15540  flodddiv4  15754  2prm  16026  unbenlem  16234  dec5dvds  16390  modxai  16394  mod2xi  16395  mod2xnegi  16397  gcdi  16399  numexp2x  16405  decsplit  16409  setsid  16530  mreexexlem3d  16909  oppchom  16977  2oppchomf  16986  isoval  17027  estrres  17381  oppchofcl  17502  oyoncl  17512  mvdco  18565  m1expaddsub  18618  psgn0fv0  18631  oppglsm  18759  dprd2da  19157  ring1  19348  opprsubg  19382  lsppratlem1  19912  zzngim  20244  cnmsgnsubg  20266  psgninv  20271  zrhpsgnmhm  20273  ply1basfvi  20870  coe1tm  20902  ply1coe  20925  neitr  21785  comppfsc  22137  kgeni  22142  xkoinjcn  22292  ufprim  22514  metreslem  22969  restmetu  23177  retopbas  23366  cnfldms  23381  qdensere2  23402  xrsmopn  23417  metdscn2  23462  pcoass  23629  recvs  23751  zclmncvs  23753  iscmet3lem3  23894  cncms  23959  cnfldcusp  23961  resscdrg  23962  rrxprds  23993  ovoliunnul  24111  uniioombllem4  24190  vitalilem5  24216  mbfres  24248  ismbf3d  24258  i1fima  24282  i1fd  24285  itg2cnlem1  24365  itgss3  24418  ellimc2  24480  limccnp2  24495  cpnres  24540  lhop  24619  plyeq0  24808  plypf1  24809  sinhalfpilem  25056  sincos6thpi  25108  sincos3rdpi  25109  pige3ALT  25112  dfrelog  25157  logimul  25205  logneg2  25206  dvlog  25242  cxpsqrt  25294  ang180lem2  25396  ang180lem3  25397  ang180lem4  25398  quart1  25442  asin1  25480  atan0  25494  atanlogsublem  25501  atan1  25514  log2tlbnd  25531  log2ublem2  25533  log2ub  25535  basellem8  25673  cht2  25757  ppiub  25788  bposlem6  25873  bposlem8  25875  bposlem9  25876  lgsdir2lem3  25911  lgseisenlem1  25959  lgseisenlem2  25960  lgsquadlem1  25964  lgsquadlem2  25965  2lgsoddprmlem2  25993  chebbnd1  26056  istrkg3ld  26255  tgcgr4  26325  motplusg  26336  ax5seglem7  26729  ex-un  28209  ex-sqrt  28239  ipdirilem  28612  ipasslem10  28622  hisubcomi  28887  normlem0  28892  norm3difi  28930  norm3lem  28932  polid2i  28940  chdmj1i  29264  chjjdiri  29307  spansn0  29324  pjoml4i  29370  cmbr3i  29383  qlaxr3i  29419  honpcani  29608  honpncani  29610  lnopunilem1  29793  lnophmlem2  29800  lnfn0i  29825  pjbdlni  29932  pjclem1  29978  pjclem3  29980  pjci  29983  atomli  30165  atabs2i  30185  mddmdin0i  30214  disjdifr  30283  difeq  30289  disjdifprg  30338  imadifxp  30364  fnresin  30385  ofpreima2  30429  df1stres  30463  df2ndres  30464  cnvoprabOLD  30482  dfdec100  30572  decdiv10  30598  dpmul100  30599  dpmul1000  30601  dpexpp1  30610  dpadd2  30612  dpadd  30613  dpmul  30615  dpmul4  30616  threehalves  30617  xrge0base  30719  xrge00  30720  xrge0mulgnn0  30723  tocycfvres1  30802  tocycfvres2  30803  cycpmfvlem  30804  cycpmfv3  30807  cycpmcl  30808  cyc2fv1  30813  cyc3conja  30849  xrge0slmod  30968  lmatfvlem  31168  xrge0iifcnv  31286  lmxrge0  31305  cnrrext  31361  qqtopn  31362  esumrnmpt2  31437  esumpfinvallem  31443  unelldsys  31527  ldgenpisyslem1  31532  measunl  31585  mbfmcst  31627  difelcarsg  31678  carsggect  31686  sibfof  31708  eulerpartlemmf  31743  fib2  31770  fib3  31771  fib4  31772  fib5  31773  fib6  31774  0rrv  31819  coinfliprv  31850  ballotlem2  31856  prodfzo03  31984  chtvalz  32010  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  kur14lem6  32571  kur14lem7  32572  cvmlift2lem12  32674  problem5  33025  quad3  33026  divcnvlin  33077  logi  33079  bj-2upln1upl  34460  bj-rest0  34508  relowlssretop  34780  relowlpssretop  34781  1oequni2o  34785  curunc  35039  ptrest  35056  poimirlem16  35073  poimirlem30  35087  mblfinlem2  35095  ovoliunnfl  35099  voliunnfl  35101  itg2addnclem2  35109  ftc1anclem5  35134  ftc1anclem6  35135  sdc  35182  heiborlem3  35251  xrnresex  35814  dvh4dimN  38743  12gcd5e1  39291  60gcd6e6  39292  60gcd7e1  39293  420gcd8e4  39294  lcmeprodgcdi  39295  lcmineqlem23  39339  3lexlogpow5ineq1  39341  sq3deccom12  39484  it1ei  39573  sn-0tie0  39576  sn-inelr  39590  dnnumch1  39988  aomclem6  40003  areaquad  40166  unitadd  40901  seff  41013  sblpnf  41014  hashnzfz  41024  lhe4.4ex1a  41033  xrtgcntopre  42118  iccdifioo  42152  itgsin0pilem1  42592  stoweidlem13  42655  stoweidlem26  42668  fourierdlem62  42810  fourierdlem102  42850  fourierdlem114  42862  fourierswlem  42872  fouriersw  42873  sge0tsms  43019  meaiuninc  43120  fmtno4prmfac  44089  41prothprm  44137  2zrngasgrp  44564  2zrngmsgrp  44571  mvlraddi  45298  mvlrmuli  45305  i2linesi  45306