Theorem eqtr3i 2768

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 2747	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2766	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  3eqtr3i  2774  3eqtr3ri  2775  rabrabiOLD  3418  unundi  4100  unundir  4101  inindi  4157  inindir  4158  dfin4  4198  difun1  4220  difabs  4224  notab  4235  dif0  4303  disjdifr  4403  difdifdir  4419  pwundif  4556  tpidm13  4689  intmin2  4903  iunxdif3  5020  univ  5361  iunxpconst  5650  opabresidOLD  5948  rnresi  5972  rnresv  6093  cnvsn0  6102  resdmres  6124  coi2  6156  coires1  6157  dfdm2  6173  isarep2  6507  resasplit  6628  ssimaex  6835  fnreseql  6907  resfunexg  7073  mpompt  7366  caov31  7479  fvresex  7776  xpexgALT  7797  1st2val  7832  2nd2val  7833  cnvoprab  7873  fnsuppeq0  7979  ecopovtrn  8567  limensuci  8889  pwfilem  8922  pssnnOLD  8969  r1sucg  9458  jech9.3  9503  rankbnd2  9558  djuin  9607  compss  10063  zorn2lem4  10186  iunfo  10226  cardf  10237  alephsuc3  10267  fpwwe2lem12  10329  rankcf  10464  halfnq  10663  addclprlem2  10704  mulgt0sr  10792  mul02lem2  11082  mul02  11083  addid1  11085  mvlladdi  11169  mvllmuli  11738  infrenegsup  11888  8th4div3  12123  nneo  12334  nummac  12411  numadd  12413  numaddc  12414  nummul1c  12415  decbin0  12506  rpsup  13514  resup  13515  om2uzrdg  13604  m1expcl2  13732  facnn  13917  fac0  13918  faclbnd4lem1  13935  4bc3eq4  13970  hasheq0  14006  f1oun2prg  14558  sqrt1  14911  sqrt4  14912  sqrt9  14913  rddif  14980  abs3lemi  15050  sumss2  15366  divcnvshft  15495  geo2sum2  15514  geomulcvg  15516  geoihalfsum  15522  risefall0lem  15664  bpoly2  15695  bpoly3  15696  sin0  15786  efival  15789  ef01bndlem  15821  cos2bnd  15825  sin4lt0  15832  flodddiv4  16050  2prm  16325  unbenlem  16537  dec5dvds  16693  modxai  16697  mod2xi  16698  mod2xnegi  16700  gcdi  16702  numexp2x  16708  decsplit  16712  setsid  16837  mreexexlem3d  17272  oppchom  17342  2oppchomf  17352  isoval  17394  estrres  17772  oppchofcl  17894  oyoncl  17904  mvdco  18968  m1expaddsub  19021  psgn0fv0  19034  oppglsm  19162  dprd2da  19560  ring1  19756  opprsubg  19793  lsppratlem1  20324  zzngim  20672  cnmsgnsubg  20694  psgninv  20699  zrhpsgnmhm  20701  ply1basfvi  21322  coe1tm  21354  ply1coe  21377  comppfsc  22591  kgeni  22596  xkoinjcn  22746  ufprim  22968  metreslem  23423  retopbas  23830  cnfldms  23845  qdensere2  23866  xrsmopn  23881  metdscn2  23926  pcoass  24093  recvs  24215  zclmncvs  24217  iscmet3lem3  24359  cncms  24424  cnfldcusp  24426  resscdrg  24427  rrxprds  24458  ovoliunnul  24576  uniioombllem4  24655  vitalilem5  24681  mbfres  24713  ismbf3d  24723  i1fima  24747  i1fd  24750  itg2cnlem1  24831  itgss3  24884  ellimc2  24946  limccnp2  24961  cpnres  25006  lhop  25085  plyeq0  25277  plypf1  25278  sinhalfpilem  25525  sincos6thpi  25577  sincos3rdpi  25578  pige3ALT  25581  dfrelog  25626  logimul  25674  logneg2  25675  dvlog  25711  cxpsqrt  25763  ang180lem2  25865  ang180lem3  25866  ang180lem4  25867  quart1  25911  asin1  25949  atan0  25963  atanlogsublem  25970  atan1  25983  log2tlbnd  26000  log2ublem2  26002  log2ub  26004  basellem8  26142  cht2  26226  ppiub  26257  bposlem6  26342  bposlem8  26344  bposlem9  26345  lgsdir2lem3  26380  lgseisenlem1  26428  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  2lgsoddprmlem2  26462  chebbnd1  26525  istrkg3ld  26726  tgcgr4  26796  motplusg  26807  ax5seglem7  27206  ex-un  28689  ex-sqrt  28719  ipdirilem  29092  ipasslem10  29102  hisubcomi  29367  normlem0  29372  norm3difi  29410  norm3lem  29412  polid2i  29420  chdmj1i  29744  chjjdiri  29787  spansn0  29804  pjoml4i  29850  cmbr3i  29863  qlaxr3i  29899  honpcani  30088  honpncani  30090  lnopunilem1  30273  lnophmlem2  30280  lnfn0i  30305  pjbdlni  30412  pjclem1  30458  pjclem3  30460  pjci  30463  atomli  30645  atabs2i  30665  mddmdin0i  30694  imadifxp  30841  fnresin  30862  ofpreima2  30905  df1stres  30938  df2ndres  30939  cnvoprabOLD  30957  dfdec100  31046  decdiv10  31072  dpmul100  31073  dpmul1000  31075  dpexpp1  31084  dpadd2  31086  dpadd  31087  dpmul  31089  dpmul4  31090  threehalves  31091  xrge0base  31196  xrge00  31197  xrge0mulgnn0  31200  cyc2fv1  31290  cyc3conja  31326  xrge0slmod  31450  lmatfvlem  31667  xrge0iifcnv  31785  lmxrge0  31804  cnrrext  31860  qqtopn  31861  esumrnmpt2  31936  esumpfinvallem  31942  unelldsys  32026  ldgenpisyslem1  32031  measunl  32084  mbfmcst  32126  difelcarsg  32177  carsggect  32185  sibfof  32207  eulerpartlemmf  32242  fib2  32269  fib3  32270  fib4  32271  fib5  32272  fib6  32273  0rrv  32318  coinfliprv  32349  ballotlem2  32355  prodfzo03  32483  chtvalz  32509  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  kur14lem6  33073  kur14lem7  33074  cvmlift2lem12  33176  problem5  33527  quad3  33528  divcnvlin  33604  logi  33606  bj-2upln1upl  35141  bj-rest0  35191  relowlssretop  35461  relowlpssretop  35462  1oequni2o  35466  curunc  35686  ptrest  35703  poimirlem16  35720  poimirlem30  35734  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  itg2addnclem2  35756  ftc1anclem5  35781  ftc1anclem6  35782  sdc  35829  heiborlem3  35898  xrnresex  36459  dvh4dimN  39388  12gcd5e1  39939  60gcd6e6  39940  60gcd7e1  39941  420gcd8e4  39942  lcmeprodgcdi  39943  lcmineqlem23  39987  acos1half  40098  sq3deccom12  40239  it1ei  40339  sn-0tie0  40342  sn-inelr  40356  dnnumch1  40785  aomclem6  40800  areaquad  40963  unitadd  41695  seff  41816  sblpnf  41817  hashnzfz  41827  lhe4.4ex1a  41836  xrtgcntopre  42909  iccdifioo  42943  itgsin0pilem1  43381  stoweidlem13  43444  stoweidlem26  43457  fourierdlem62  43599  fourierdlem102  43639  fourierdlem114  43651  fourierswlem  43661  fouriersw  43662  sge0tsms  43808  meaiuninc  43909  fmtno4prmfac  44912  41prothprm  44959  2zrngasgrp  45386  2zrngmsgrp  45393  mvlraddi  46360  mvlrmuli  46367  i2linesi  46368