Theorem eqtr3i 2755

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 2739	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2753	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  3eqtr3i  2761  3eqtr3ri  2762  unundi  4142  unundir  4143  inindi  4201  inindir  4202  dfin4  4244  difun1  4265  difabs  4269  notab  4280  dif0  4344  disjdifr  4439  difdifdir  4458  pwundif  4590  tpidm13  4723  intmin2  4942  iunxdif3  5062  univ  5414  iunxpconst  5714  rnresi  6049  rnresv  6177  cnvsn0  6186  resdmres  6208  coi2  6239  coires1  6240  dfdm2  6257  isarep2  6611  resasplit  6733  ssimaex  6949  fnreseql  7023  resfunexg  7192  mpompt  7506  caov31  7621  fvresex  7941  xpexgALT  7963  1st2val  7999  2nd2val  8000  cnvoprab  8042  fnsuppeq0  8174  ecopovtrn  8796  limensuci  9123  pwfilem  9274  r1sucg  9729  jech9.3  9774  rankbnd2  9829  djuin  9878  compss  10336  zorn2lem4  10459  iunfo  10499  cardf  10510  alephsuc3  10540  fpwwe2lem12  10602  rankcf  10737  halfnq  10936  addclprlem2  10977  mulgt0sr  11065  mul02lem2  11358  mul02  11359  addrid  11361  mvlladdi  11447  mvllmuli  12022  infrenegsup  12173  8th4div3  12409  halfpm6th  12411  nneo  12625  nummac  12701  numadd  12703  numaddc  12704  nummul1c  12705  decbin0  12796  rpsup  13835  resup  13836  om2uzrdg  13928  m1expcl2  14057  facnn  14247  fac0  14248  faclbnd4lem1  14265  4bc3eq4  14300  hasheq0  14335  f1oun2prg  14890  sqrt1  15244  sqrt4  15245  sqrt9  15246  rddif  15314  abs3lemi  15384  sumss2  15699  divcnvshft  15828  geo2sum2  15847  geomulcvg  15849  geoihalfsum  15855  risefall0lem  15999  bpoly2  16030  bpoly3  16031  sin0  16124  efival  16127  ef01bndlem  16159  cos2bnd  16163  sin4lt0  16170  flodddiv4  16392  2prm  16669  unbenlem  16886  dec5dvds  17042  modxai  17046  mod2xi  17047  mod2xnegi  17049  gcdi  17051  numexp2x  17056  decsplit  17060  setsid  17184  mreexexlem3d  17614  oppchom  17683  2oppchomf  17692  isoval  17734  estrres  18107  oppchofcl  18228  oyoncl  18238  mvdco  19382  m1expaddsub  19435  psgn0fv0  19448  oppglsm  19579  dprd2da  19981  ring1  20226  opprsubg  20268  lsppratlem1  21064  pzriprnglem7  21404  zzngim  21469  cnmsgnsubg  21493  psgninv  21498  zrhpsgnmhm  21500  ply1basfvi  22132  coe1tm  22166  ply1coe  22192  comppfsc  23426  kgeni  23431  xkoinjcn  23581  ufprim  23803  metreslem  24257  retopbas  24655  cnfldms  24670  qdensere2  24692  xrsmopn  24708  metdscn2  24753  pcoass  24931  recvs  25053  zclmncvs  25055  iscmet3lem3  25197  cncms  25262  cnfldcusp  25264  resscdrg  25265  rrxprds  25296  ovoliunnul  25415  uniioombllem4  25494  vitalilem5  25520  mbfres  25552  ismbf3d  25562  i1fima  25586  i1fd  25589  itg2cnlem1  25669  itgss3  25723  ellimc2  25785  limccnp2  25800  cpnres  25846  lhop  25928  plyeq0  26123  plypf1  26124  sinhalfpilem  26379  sincos6thpi  26432  sincos3rdpi  26433  pige3ALT  26436  dfrelog  26481  logi  26503  logimul  26530  logneg2  26531  dvlog  26567  cxpsqrt  26619  ang180lem2  26727  ang180lem3  26728  ang180lem4  26729  quart1  26773  asin1  26811  atan0  26825  atanlogsublem  26832  atan1  26845  log2tlbnd  26862  log2ublem2  26864  log2ub  26866  basellem8  27005  cht2  27089  ppiub  27122  bposlem6  27207  bposlem8  27209  bposlem9  27210  lgsdir2lem3  27245  lgseisenlem1  27293  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  2lgsoddprmlem2  27327  chebbnd1  27390  negsbdaylem  27969  om2noseqrdg  28205  zseo  28315  istrkg3ld  28395  tgcgr4  28465  motplusg  28476  ax5seglem7  28869  ex-un  30360  ex-sqrt  30390  ipdirilem  30765  ipasslem10  30775  hisubcomi  31040  normlem0  31045  norm3difi  31083  norm3lem  31085  polid2i  31093  chdmj1i  31417  chjjdiri  31460  spansn0  31477  pjoml4i  31523  cmbr3i  31536  qlaxr3i  31572  honpcani  31761  honpncani  31763  lnopunilem1  31946  lnophmlem2  31953  lnfn0i  31978  pjbdlni  32085  pjclem1  32131  pjclem3  32133  pjci  32136  atomli  32318  atabs2i  32338  mddmdin0i  32367  imadifxp  32537  fnresin  32557  ofpreima2  32597  df1stres  32634  df2ndres  32635  nn0disj01  32750  dfdec100  32762  decdiv10  32823  dpmul100  32824  dpmul1000  32826  dpexpp1  32835  dpadd2  32837  dpadd  32838  dpmul  32840  dpmul4  32841  threehalves  32842  xrge0base  32959  xrge00  32960  xrge0mulgnn0  32963  cyc2fv1  33085  cyc3conja  33121  elrgspnlem4  33203  xrge0slmod  33326  opprqusplusg  33467  opprqusmulr  33469  2sqr3nconstr  33778  cos9thpiminplylem1  33779  cos9thpiminplylem5  33783  cos9thpinconstrlem2  33787  lmatfvlem  33812  xrge0iifcnv  33930  lmxrge0  33949  cnrrext  34007  qqtopn  34008  esumrnmpt2  34065  esumpfinvallem  34071  unelldsys  34155  ldgenpisyslem1  34160  measunl  34213  mbfmcst  34257  difelcarsg  34308  carsggect  34316  sibfof  34338  eulerpartlemmf  34373  fib2  34400  fib3  34401  fib4  34402  fib5  34403  fib6  34404  0rrv  34449  coinfliprv  34481  ballotlem2  34487  prodfzo03  34601  chtvalz  34627  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  kur14lem6  35205  kur14lem7  35206  cvmlift2lem12  35308  problem5  35663  quad3  35664  divcnvlin  35727  in-ax8  36219  bj-2upln1upl  37019  bj-rest0  37088  relowlssretop  37358  relowlpssretop  37359  1oequni2o  37363  curunc  37603  ptrest  37620  poimirlem16  37637  poimirlem30  37651  mblfinlem2  37659  ovoliunnfl  37663  voliunnfl  37665  itg2addnclem2  37673  ftc1anclem5  37698  ftc1anclem6  37699  sdc  37745  heiborlem3  37814  xrnresex  38399  dmxrncnvepres  38402  dvh4dimN  41448  12gcd5e1  41998  60gcd6e6  41999  60gcd7e1  42000  420gcd8e4  42001  lcmeprodgcdi  42002  lcmineqlem23  42046  sq3deccom12  42285  asin1half  42352  acos1half  42353  redvmptabs  42355  readvrec  42357  sn-it1ei  42432  sn-0tie0  42446  dnnumch1  43040  aomclem6  43055  areaquad  43212  naddov4  43379  unitadd  44191  seff  44305  sblpnf  44306  hashnzfz  44316  lhe4.4ex1a  44325  xrtgcntopre  45481  iccdifioo  45520  itgsin0pilem1  45955  stoweidlem13  46018  stoweidlem26  46031  fourierdlem62  46173  fourierdlem102  46213  fourierdlem114  46225  fourierswlem  46235  fouriersw  46236  sge0tsms  46385  meaiuninc  46486  tworepnotupword  46891  fmtno4prmfac  47577  41prothprm  47624  dfclnbgr4  47829  2zrngasgrp  48238  2zrngmsgrp  48245  tposres3  48873  eloppf  49126  setc1onsubc  49595  mvlraddi  49764  mvlrmuli  49770  i2linesi  49771