Theorem eqtr3i 2769

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  3eqtr3i  2775  3eqtr3ri  2776  rabrabiOLD  3429  unundi  4105  unundir  4106  inindi  4161  inindir  4162  dfin4  4202  difun1  4224  difabs  4228  notab  4239  dif0  4307  disjdifr  4407  difdifdir  4423  pwundif  4560  tpidm13  4693  intmin2  4907  iunxdif3  5025  univ  5368  iunxpconst  5660  opabresidOLD  5962  rnresi  5986  rnresv  6109  cnvsn0  6118  resdmres  6140  coi2  6171  coires1  6172  dfdm2  6188  isarep2  6532  resasplit  6653  ssimaex  6862  fnreseql  6934  resfunexg  7100  mpompt  7397  caov31  7510  fvresex  7811  xpexgALT  7833  1st2val  7868  2nd2val  7869  cnvoprab  7909  fnsuppeq0  8017  ecopovtrn  8618  limensuci  8949  pwfilem  8969  pssnnOLD  9049  r1sucg  9536  jech9.3  9581  rankbnd2  9636  djuin  9685  compss  10141  zorn2lem4  10264  iunfo  10304  cardf  10315  alephsuc3  10345  fpwwe2lem12  10407  rankcf  10542  halfnq  10741  addclprlem2  10782  mulgt0sr  10870  mul02lem2  11161  mul02  11162  addid1  11164  mvlladdi  11248  mvllmuli  11817  infrenegsup  11967  8th4div3  12202  nneo  12413  nummac  12491  numadd  12493  numaddc  12494  nummul1c  12495  decbin0  12586  rpsup  13595  resup  13596  om2uzrdg  13685  m1expcl2  13813  facnn  13998  fac0  13999  faclbnd4lem1  14016  4bc3eq4  14051  hasheq0  14087  f1oun2prg  14639  sqrt1  14992  sqrt4  14993  sqrt9  14994  rddif  15061  abs3lemi  15131  sumss2  15447  divcnvshft  15576  geo2sum2  15595  geomulcvg  15597  geoihalfsum  15603  risefall0lem  15745  bpoly2  15776  bpoly3  15777  sin0  15867  efival  15870  ef01bndlem  15902  cos2bnd  15906  sin4lt0  15913  flodddiv4  16131  2prm  16406  unbenlem  16618  dec5dvds  16774  modxai  16778  mod2xi  16779  mod2xnegi  16781  gcdi  16783  numexp2x  16789  decsplit  16793  setsid  16918  mreexexlem3d  17364  oppchom  17434  2oppchomf  17444  isoval  17486  estrres  17865  oppchofcl  17987  oyoncl  17997  mvdco  19062  m1expaddsub  19115  psgn0fv0  19128  oppglsm  19256  dprd2da  19654  ring1  19850  opprsubg  19887  lsppratlem1  20418  zzngim  20769  cnmsgnsubg  20791  psgninv  20796  zrhpsgnmhm  20798  ply1basfvi  21421  coe1tm  21453  ply1coe  21476  comppfsc  22692  kgeni  22697  xkoinjcn  22847  ufprim  23069  metreslem  23524  retopbas  23933  cnfldms  23948  qdensere2  23969  xrsmopn  23984  metdscn2  24029  pcoass  24196  recvs  24318  recvsOLD  24319  zclmncvs  24321  iscmet3lem3  24463  cncms  24528  cnfldcusp  24530  resscdrg  24531  rrxprds  24562  ovoliunnul  24680  uniioombllem4  24759  vitalilem5  24785  mbfres  24817  ismbf3d  24827  i1fima  24851  i1fd  24854  itg2cnlem1  24935  itgss3  24988  ellimc2  25050  limccnp2  25065  cpnres  25110  lhop  25189  plyeq0  25381  plypf1  25382  sinhalfpilem  25629  sincos6thpi  25681  sincos3rdpi  25682  pige3ALT  25685  dfrelog  25730  logimul  25778  logneg2  25779  dvlog  25815  cxpsqrt  25867  ang180lem2  25969  ang180lem3  25970  ang180lem4  25971  quart1  26015  asin1  26053  atan0  26067  atanlogsublem  26074  atan1  26087  log2tlbnd  26104  log2ublem2  26106  log2ub  26108  basellem8  26246  cht2  26330  ppiub  26361  bposlem6  26446  bposlem8  26448  bposlem9  26449  lgsdir2lem3  26484  lgseisenlem1  26532  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  2lgsoddprmlem2  26566  chebbnd1  26629  istrkg3ld  26831  tgcgr4  26901  motplusg  26912  ax5seglem7  27312  ex-un  28797  ex-sqrt  28827  ipdirilem  29200  ipasslem10  29210  hisubcomi  29475  normlem0  29480  norm3difi  29518  norm3lem  29520  polid2i  29528  chdmj1i  29852  chjjdiri  29895  spansn0  29912  pjoml4i  29958  cmbr3i  29971  qlaxr3i  30007  honpcani  30196  honpncani  30198  lnopunilem1  30381  lnophmlem2  30388  lnfn0i  30413  pjbdlni  30520  pjclem1  30566  pjclem3  30568  pjci  30571  atomli  30753  atabs2i  30773  mddmdin0i  30802  imadifxp  30949  fnresin  30970  ofpreima2  31012  df1stres  31045  df2ndres  31046  cnvoprabOLD  31064  dfdec100  31153  decdiv10  31179  dpmul100  31180  dpmul1000  31182  dpexpp1  31191  dpadd2  31193  dpadd  31194  dpmul  31196  dpmul4  31197  threehalves  31198  xrge0base  31303  xrge00  31304  xrge0mulgnn0  31307  cyc2fv1  31397  cyc3conja  31433  xrge0slmod  31557  lmatfvlem  31774  xrge0iifcnv  31892  lmxrge0  31911  cnrrext  31969  qqtopn  31970  esumrnmpt2  32045  esumpfinvallem  32051  unelldsys  32135  ldgenpisyslem1  32140  measunl  32193  mbfmcst  32235  difelcarsg  32286  carsggect  32294  sibfof  32316  eulerpartlemmf  32351  fib2  32378  fib3  32379  fib4  32380  fib5  32381  fib6  32382  0rrv  32427  coinfliprv  32458  ballotlem2  32464  prodfzo03  32592  chtvalz  32618  hgt750lemd  32637  hgt750lem  32640  hgt750lem2  32641  kur14lem6  33182  kur14lem7  33183  cvmlift2lem12  33285  problem5  33636  quad3  33637  divcnvlin  33707  logi  33709  bj-2upln1upl  35223  bj-rest0  35273  relowlssretop  35543  relowlpssretop  35544  1oequni2o  35548  curunc  35768  ptrest  35785  poimirlem16  35802  poimirlem30  35816  mblfinlem2  35824  ovoliunnfl  35828  voliunnfl  35830  itg2addnclem2  35838  ftc1anclem5  35863  ftc1anclem6  35864  sdc  35911  heiborlem3  35980  xrnresex  36539  dvh4dimN  39468  12gcd5e1  40018  60gcd6e6  40019  60gcd7e1  40020  420gcd8e4  40021  lcmeprodgcdi  40022  lcmineqlem23  40066  acos1half  40177  sq3deccom12  40325  it1ei  40425  sn-0tie0  40428  sn-inelr  40442  dnnumch1  40876  aomclem6  40891  areaquad  41054  unitadd  41813  seff  41934  sblpnf  41935  hashnzfz  41945  lhe4.4ex1a  41954  xrtgcntopre  43026  iccdifioo  43060  itgsin0pilem1  43498  stoweidlem13  43561  stoweidlem26  43574  fourierdlem62  43716  fourierdlem102  43756  fourierdlem114  43768  fourierswlem  43778  fouriersw  43779  sge0tsms  43925  meaiuninc  44026  fmtno4prmfac  45035  41prothprm  45082  2zrngasgrp  45509  2zrngmsgrp  45516  mvlraddi  46485  mvlrmuli  46492  i2linesi  46493  tworepnotupword  46532