Theorem eqtr3i 2767

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  3eqtr3i  2773  3eqtr3ri  2774  unundi  4176  unundir  4177  inindi  4235  inindir  4236  dfin4  4278  difun1  4299  difabs  4303  notab  4314  dif0  4378  disjdifr  4473  difdifdir  4492  pwundif  4624  tpidm13  4756  intmin2  4975  iunxdif3  5095  univ  5456  iunxpconst  5758  rnresi  6093  rnresv  6221  cnvsn0  6230  resdmres  6252  coi2  6283  coires1  6284  dfdm2  6301  isarep2  6658  resasplit  6778  ssimaex  6994  fnreseql  7068  resfunexg  7235  mpompt  7547  caov31  7662  fvresex  7984  xpexgALT  8006  1st2val  8042  2nd2val  8043  cnvoprab  8085  fnsuppeq0  8217  ecopovtrn  8860  limensuci  9193  pwfilem  9356  r1sucg  9809  jech9.3  9854  rankbnd2  9909  djuin  9958  compss  10416  zorn2lem4  10539  iunfo  10579  cardf  10590  alephsuc3  10620  fpwwe2lem12  10682  rankcf  10817  halfnq  11016  addclprlem2  11057  mulgt0sr  11145  mul02lem2  11438  mul02  11439  addrid  11441  mvlladdi  11527  mvllmuli  12100  infrenegsup  12251  8th4div3  12486  nneo  12702  nummac  12778  numadd  12780  numaddc  12781  nummul1c  12782  decbin0  12873  rpsup  13906  resup  13907  om2uzrdg  13997  m1expcl2  14126  facnn  14314  fac0  14315  faclbnd4lem1  14332  4bc3eq4  14367  hasheq0  14402  f1oun2prg  14956  sqrt1  15310  sqrt4  15311  sqrt9  15312  rddif  15379  abs3lemi  15449  sumss2  15762  divcnvshft  15891  geo2sum2  15910  geomulcvg  15912  geoihalfsum  15918  risefall0lem  16062  bpoly2  16093  bpoly3  16094  sin0  16185  efival  16188  ef01bndlem  16220  cos2bnd  16224  sin4lt0  16231  flodddiv4  16452  2prm  16729  unbenlem  16946  dec5dvds  17102  modxai  17106  mod2xi  17107  mod2xnegi  17109  gcdi  17111  numexp2x  17116  decsplit  17120  setsid  17244  mreexexlem3d  17689  oppchom  17758  2oppchomf  17767  isoval  17809  estrres  18184  oppchofcl  18305  oyoncl  18315  mvdco  19463  m1expaddsub  19516  psgn0fv0  19529  oppglsm  19660  dprd2da  20062  ring1  20307  opprsubg  20352  lsppratlem1  21149  pzriprnglem7  21498  zzngim  21571  cnmsgnsubg  21595  psgninv  21600  zrhpsgnmhm  21602  ply1basfvi  22242  coe1tm  22276  ply1coe  22302  comppfsc  23540  kgeni  23545  xkoinjcn  23695  ufprim  23917  metreslem  24372  retopbas  24781  cnfldms  24796  qdensere2  24818  xrsmopn  24834  metdscn2  24879  pcoass  25057  recvs  25179  recvsOLD  25180  zclmncvs  25182  iscmet3lem3  25324  cncms  25389  cnfldcusp  25391  resscdrg  25392  rrxprds  25423  ovoliunnul  25542  uniioombllem4  25621  vitalilem5  25647  mbfres  25679  ismbf3d  25689  i1fima  25713  i1fd  25716  itg2cnlem1  25796  itgss3  25850  ellimc2  25912  limccnp2  25927  cpnres  25973  lhop  26055  plyeq0  26250  plypf1  26251  sinhalfpilem  26505  sincos6thpi  26558  sincos3rdpi  26559  pige3ALT  26562  dfrelog  26607  logi  26629  logimul  26656  logneg2  26657  dvlog  26693  cxpsqrt  26745  ang180lem2  26853  ang180lem3  26854  ang180lem4  26855  quart1  26899  asin1  26937  atan0  26951  atanlogsublem  26958  atan1  26971  log2tlbnd  26988  log2ublem2  26990  log2ub  26992  basellem8  27131  cht2  27215  ppiub  27248  bposlem6  27333  bposlem8  27335  bposlem9  27336  lgsdir2lem3  27371  lgseisenlem1  27419  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  2lgsoddprmlem2  27453  chebbnd1  27516  negsbdaylem  28088  om2noseqrdg  28310  zseo  28406  istrkg3ld  28469  tgcgr4  28539  motplusg  28550  ax5seglem7  28950  ex-un  30443  ex-sqrt  30473  ipdirilem  30848  ipasslem10  30858  hisubcomi  31123  normlem0  31128  norm3difi  31166  norm3lem  31168  polid2i  31176  chdmj1i  31500  chjjdiri  31543  spansn0  31560  pjoml4i  31606  cmbr3i  31619  qlaxr3i  31655  honpcani  31844  honpncani  31846  lnopunilem1  32029  lnophmlem2  32036  lnfn0i  32061  pjbdlni  32168  pjclem1  32214  pjclem3  32216  pjci  32219  atomli  32401  atabs2i  32421  mddmdin0i  32450  imadifxp  32614  fnresin  32636  ofpreima2  32676  df1stres  32713  df2ndres  32714  nn0disj01  32820  dfdec100  32832  decdiv10  32878  dpmul100  32879  dpmul1000  32881  dpexpp1  32890  dpadd2  32892  dpadd  32893  dpmul  32895  dpmul4  32896  threehalves  32897  xrge0base  33016  xrge00  33017  xrge0mulgnn0  33020  cyc2fv1  33141  cyc3conja  33177  elrgspnlem4  33249  xrge0slmod  33376  opprqusplusg  33517  opprqusmulr  33519  lmatfvlem  33814  xrge0iifcnv  33932  lmxrge0  33951  cnrrext  34011  qqtopn  34012  esumrnmpt2  34069  esumpfinvallem  34075  unelldsys  34159  ldgenpisyslem1  34164  measunl  34217  mbfmcst  34261  difelcarsg  34312  carsggect  34320  sibfof  34342  eulerpartlemmf  34377  fib2  34404  fib3  34405  fib4  34406  fib5  34407  fib6  34408  0rrv  34453  coinfliprv  34485  ballotlem2  34491  prodfzo03  34618  chtvalz  34644  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  kur14lem6  35216  kur14lem7  35217  cvmlift2lem12  35319  problem5  35674  quad3  35675  divcnvlin  35733  in-ax8  36225  bj-2upln1upl  37025  bj-rest0  37094  relowlssretop  37364  relowlpssretop  37365  1oequni2o  37369  curunc  37609  ptrest  37626  poimirlem16  37643  poimirlem30  37657  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  itg2addnclem2  37679  ftc1anclem5  37704  ftc1anclem6  37705  sdc  37751  heiborlem3  37820  xrnresex  38407  dvh4dimN  41449  12gcd5e1  42004  60gcd6e6  42005  60gcd7e1  42006  420gcd8e4  42007  lcmeprodgcdi  42008  lcmineqlem23  42052  sq3deccom12  42325  asin1half  42387  acos1half  42388  redvmptabs  42390  readvrec  42392  sn-it1ei  42466  sn-0tie0  42469  sn-inelr  42497  dnnumch1  43056  aomclem6  43071  areaquad  43228  naddov4  43396  unitadd  44208  seff  44328  sblpnf  44329  hashnzfz  44339  lhe4.4ex1a  44348  xrtgcntopre  45489  iccdifioo  45528  itgsin0pilem1  45965  stoweidlem13  46028  stoweidlem26  46041  fourierdlem62  46183  fourierdlem102  46223  fourierdlem114  46235  fourierswlem  46245  fouriersw  46246  sge0tsms  46395  meaiuninc  46496  tworepnotupword  46901  fmtno4prmfac  47559  41prothprm  47606  dfclnbgr4  47811  2zrngasgrp  48162  2zrngmsgrp  48169  tposres3  48781  mvlraddi  49290  mvlrmuli  49296  i2linesi  49297