Theorem eqtr3i 2756

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  3eqtr3i  2762  3eqtr3ri  2763  unundi  4123  unundir  4124  inindi  4182  inindir  4183  dfin4  4225  difun1  4246  difabs  4250  notab  4261  dif0  4325  disjdifr  4420  difdifdir  4439  pwundif  4571  tpidm13  4706  intmin2  4923  iunxdif3  5041  univ  5390  iunxpconst  5687  rnresi  6023  rnresv  6148  cnvsn0  6157  resdmres  6179  coi2  6211  coires1  6212  dfdm2  6228  isarep2  6571  resasplit  6693  ssimaex  6907  fnreseql  6981  resfunexg  7149  mpompt  7460  caov31  7575  fvresex  7892  xpexgALT  7913  1st2val  7949  2nd2val  7950  cnvoprab  7992  fnsuppeq0  8122  ecopovtrn  8744  limensuci  9066  pwfilem  9202  r1sucg  9662  jech9.3  9707  rankbnd2  9762  djuin  9811  compss  10267  zorn2lem4  10390  iunfo  10430  cardf  10441  alephsuc3  10471  fpwwe2lem12  10533  rankcf  10668  halfnq  10867  addclprlem2  10908  mulgt0sr  10996  mul02lem2  11290  mul02  11291  addrid  11293  mvlladdi  11379  mvllmuli  11954  infrenegsup  12105  8th4div3  12341  halfpm6th  12343  nneo  12557  nummac  12633  numadd  12635  numaddc  12636  nummul1c  12637  decbin0  12728  rpsup  13770  resup  13771  om2uzrdg  13863  m1expcl2  13992  facnn  14182  fac0  14183  faclbnd4lem1  14200  4bc3eq4  14235  hasheq0  14270  f1oun2prg  14824  sqrt1  15178  sqrt4  15179  sqrt9  15180  rddif  15248  abs3lemi  15318  sumss2  15633  divcnvshft  15762  geo2sum2  15781  geomulcvg  15783  geoihalfsum  15789  risefall0lem  15933  bpoly2  15964  bpoly3  15965  sin0  16058  efival  16061  ef01bndlem  16093  cos2bnd  16097  sin4lt0  16104  flodddiv4  16326  2prm  16603  unbenlem  16820  dec5dvds  16976  modxai  16980  mod2xi  16981  mod2xnegi  16983  gcdi  16985  numexp2x  16990  decsplit  16994  setsid  17118  xrge0base  17511  mreexexlem3d  17552  oppchom  17621  2oppchomf  17630  isoval  17672  estrres  18045  oppchofcl  18166  oyoncl  18176  mvdco  19357  m1expaddsub  19410  psgn0fv0  19423  oppglsm  19554  dprd2da  19956  ring1  20228  opprsubg  20270  lsppratlem1  21084  pzriprnglem7  21424  zzngim  21489  cnmsgnsubg  21514  psgninv  21519  zrhpsgnmhm  21521  ply1basfvi  22153  coe1tm  22187  ply1coe  22213  comppfsc  23447  kgeni  23452  xkoinjcn  23602  ufprim  23824  metreslem  24277  retopbas  24675  cnfldms  24690  qdensere2  24712  xrsmopn  24728  metdscn2  24773  pcoass  24951  recvs  25073  zclmncvs  25075  iscmet3lem3  25217  cncms  25282  cnfldcusp  25284  resscdrg  25285  rrxprds  25316  ovoliunnul  25435  uniioombllem4  25514  vitalilem5  25540  mbfres  25572  ismbf3d  25582  i1fima  25606  i1fd  25609  itg2cnlem1  25689  itgss3  25743  ellimc2  25805  limccnp2  25820  cpnres  25866  lhop  25948  plyeq0  26143  plypf1  26144  sinhalfpilem  26399  sincos6thpi  26452  sincos3rdpi  26453  pige3ALT  26456  dfrelog  26501  logi  26523  logimul  26550  logneg2  26551  dvlog  26587  cxpsqrt  26639  ang180lem2  26747  ang180lem3  26748  ang180lem4  26749  quart1  26793  asin1  26831  atan0  26845  atanlogsublem  26852  atan1  26865  log2tlbnd  26882  log2ublem2  26884  log2ub  26886  basellem8  27025  cht2  27109  ppiub  27142  bposlem6  27227  bposlem8  27229  bposlem9  27230  lgsdir2lem3  27265  lgseisenlem1  27313  lgseisenlem2  27314  lgsquadlem1  27318  lgsquadlem2  27319  2lgsoddprmlem2  27347  chebbnd1  27410  negsbdaylem  27998  om2noseqrdg  28234  zseo  28345  istrkg3ld  28439  tgcgr4  28509  motplusg  28520  ax5seglem7  28913  ex-un  30404  ex-sqrt  30434  ipdirilem  30809  ipasslem10  30819  hisubcomi  31084  normlem0  31089  norm3difi  31127  norm3lem  31129  polid2i  31137  chdmj1i  31461  chjjdiri  31504  spansn0  31521  pjoml4i  31567  cmbr3i  31580  qlaxr3i  31616  honpcani  31805  honpncani  31807  lnopunilem1  31990  lnophmlem2  31997  lnfn0i  32022  pjbdlni  32129  pjclem1  32175  pjclem3  32177  pjci  32180  atomli  32362  atabs2i  32382  mddmdin0i  32411  imadifxp  32581  fnresin  32607  ofpreima2  32648  df1stres  32685  df2ndres  32686  nn0disj01  32801  dfdec100  32813  decdiv10  32876  dpmul100  32877  dpmul1000  32879  dpexpp1  32888  dpadd2  32890  dpadd  32891  dpmul  32893  dpmul4  32894  threehalves  32895  xrge00  32995  xrge0mulgnn0  32996  cyc2fv1  33090  cyc3conja  33126  elrgspnlem4  33212  xrge0slmod  33313  opprqusplusg  33454  opprqusmulr  33456  2sqr3nconstr  33794  cos9thpiminplylem1  33795  cos9thpiminplylem5  33799  cos9thpinconstrlem2  33803  lmatfvlem  33828  xrge0iifcnv  33946  lmxrge0  33965  cnrrext  34023  qqtopn  34024  esumrnmpt2  34081  esumpfinvallem  34087  unelldsys  34171  ldgenpisyslem1  34176  measunl  34229  mbfmcst  34272  difelcarsg  34323  carsggect  34331  sibfof  34353  eulerpartlemmf  34388  fib2  34415  fib3  34416  fib4  34417  fib5  34418  fib6  34419  0rrv  34464  coinfliprv  34496  ballotlem2  34502  prodfzo03  34616  chtvalz  34642  hgt750lemd  34661  hgt750lem  34664  hgt750lem2  34665  kur14lem6  35255  kur14lem7  35256  cvmlift2lem12  35358  problem5  35713  quad3  35714  divcnvlin  35777  in-ax8  36266  bj-2upln1upl  37066  bj-rest0  37135  relowlssretop  37405  relowlpssretop  37406  1oequni2o  37410  curunc  37650  ptrest  37667  poimirlem16  37684  poimirlem30  37698  mblfinlem2  37706  ovoliunnfl  37710  voliunnfl  37712  itg2addnclem2  37720  ftc1anclem5  37745  ftc1anclem6  37746  sdc  37792  heiborlem3  37861  xrnresex  38446  dmxrncnvepres  38449  dvh4dimN  41494  12gcd5e1  42044  60gcd6e6  42045  60gcd7e1  42046  420gcd8e4  42047  lcmeprodgcdi  42048  lcmineqlem23  42092  sq3deccom12  42331  asin1half  42398  acos1half  42399  redvmptabs  42401  readvrec  42403  sn-it1ei  42478  sn-0tie0  42492  dnnumch1  43085  aomclem6  43100  areaquad  43257  naddov4  43424  unitadd  44236  seff  44350  sblpnf  44351  hashnzfz  44361  lhe4.4ex1a  44370  xrtgcntopre  45524  iccdifioo  45563  itgsin0pilem1  45996  stoweidlem13  46059  stoweidlem26  46072  fourierdlem62  46214  fourierdlem102  46254  fourierdlem114  46266  fourierswlem  46276  fouriersw  46277  sge0tsms  46426  meaiuninc  46527  fmtno4prmfac  47611  41prothprm  47658  dfclnbgr4  47863  2zrngasgrp  48285  2zrngmsgrp  48292  tposres3  48920  eloppf  49173  setc1onsubc  49642  mvlraddi  49811  mvlrmuli  49817  i2linesi  49818