Theorem eqtr3i 2764

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 2762	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  3eqtr3i  2770  3eqtr3ri  2771  unundi  4105  unundir  4106  inindi  4163  inindir  4164  dfin4  4206  difun1  4227  difabs  4231  notab  4242  dif0  4306  difdifdir  4419  pwundif  4553  tpidm13  4688  intmin2  4905  iunxdif3  5024  univ  5390  iunxpconst  5691  rnresi  6027  rnresv  6152  cnvsn0  6161  resdmres  6183  coi2  6215  coires1  6216  dfdm2  6232  isarep2  6575  resasplit  6697  ssimaex  6912  fnreseql  6989  resfunexg  7159  mpompt  7470  caov31  7585  fvresex  7902  xpexgALT  7923  1st2val  7959  2nd2val  7960  cnvoprab  8002  fnsuppeq0  8132  ecopovtrn  8757  limensuci  9081  pwfilem  9218  r1sucg  9684  jech9.3  9729  rankbnd2  9784  djuin  9833  compss  10289  zorn2lem4  10412  iunfo  10452  cardf  10463  alephsuc3  10494  fpwwe2lem12  10556  rankcf  10691  halfnq  10890  addclprlem2  10931  mulgt0sr  11019  mul02lem2  11314  mul02  11315  addrid  11317  mvlladdi  11403  mvllmuli  11979  infrenegsup  12130  8th4div3  12388  halfpm6th  12390  nneo  12604  nummac  12680  numadd  12682  numaddc  12683  nummul1c  12684  decbin0  12775  rpsup  13816  resup  13817  om2uzrdg  13909  m1expcl2  14038  facnn  14228  fac0  14229  faclbnd4lem1  14246  4bc3eq4  14281  hasheq0  14316  f1oun2prg  14870  sqrt1  15224  sqrt4  15225  sqrt9  15226  rddif  15294  abs3lemi  15364  sumss2  15679  divcnvshft  15811  geo2sum2  15830  geomulcvg  15832  geoihalfsum  15838  risefall0lem  15982  bpoly2  16013  bpoly3  16014  sin0  16107  efival  16110  ef01bndlem  16142  cos2bnd  16146  sin4lt0  16153  flodddiv4  16375  2prm  16652  unbenlem  16870  dec5dvds  17026  modxai  17030  mod2xi  17031  mod2xnegi  17033  gcdi  17035  numexp2x  17040  decsplit  17044  setsid  17168  xrge0base  17562  mreexexlem3d  17603  oppchom  17672  2oppchomf  17681  isoval  17723  estrres  18096  oppchofcl  18217  oyoncl  18227  mvdco  19411  m1expaddsub  19464  psgn0fv0  19477  oppglsm  19608  dprd2da  20010  ring1  20282  opprsubg  20323  lsppratlem1  21140  pzriprnglem7  21462  zzngim  21527  cnmsgnsubg  21552  psgninv  21557  zrhpsgnmhm  21559  ply1basfvi  22225  coe1tm  22259  ply1coe  22284  comppfsc  23515  kgeni  23520  xkoinjcn  23670  ufprim  23892  metreslem  24345  retopbas  24743  cnfldms  24758  qdensere2  24780  xrsmopn  24796  metdscn2  24841  pcoass  25009  recvs  25131  zclmncvs  25133  iscmet3lem3  25275  cncms  25340  cnfldcusp  25342  resscdrg  25343  rrxprds  25374  ovoliunnul  25492  uniioombllem4  25571  vitalilem5  25597  mbfres  25629  ismbf3d  25639  i1fima  25663  i1fd  25666  itg2cnlem1  25746  itgss3  25800  ellimc2  25862  limccnp2  25877  cpnres  25922  lhop  26001  plyeq0  26194  plypf1  26195  sinhalfpilem  26445  sincos6thpi  26498  sincos3rdpi  26499  pige3ALT  26502  dfrelog  26547  logi  26569  logimul  26596  logneg2  26597  dvlog  26633  cxpsqrt  26685  ang180lem2  26792  ang180lem3  26793  ang180lem4  26794  quart1  26838  asin1  26876  atan0  26890  atanlogsublem  26897  atan1  26910  log2tlbnd  26927  log2ublem2  26929  log2ub  26931  basellem8  27069  cht2  27153  ppiub  27185  bposlem6  27270  bposlem8  27272  bposlem9  27273  lgsdir2lem3  27308  lgseisenlem1  27356  lgseisenlem2  27357  lgsquadlem1  27361  lgsquadlem2  27362  2lgsoddprmlem2  27390  chebbnd1  27453  negbdaylem  28066  om2noseqrdg  28314  zseo  28432  bdaypw2n0bndlem  28473  istrkg3ld  28547  tgcgr4  28617  motplusg  28628  ax5seglem7  29022  ex-un  30512  ex-sqrt  30542  ipdirilem  30918  ipasslem10  30928  hisubcomi  31193  normlem0  31198  norm3difi  31236  norm3lem  31238  polid2i  31246  chdmj1i  31570  chjjdiri  31613  spansn0  31630  pjoml4i  31676  cmbr3i  31689  qlaxr3i  31725  honpcani  31914  honpncani  31916  lnopunilem1  32099  lnophmlem2  32106  lnfn0i  32131  pjbdlni  32238  pjclem1  32284  pjclem3  32286  pjci  32289  atomli  32471  atabs2i  32491  mddmdin0i  32520  imadifxp  32690  fnresin  32716  ofpreima2  32758  df1stres  32796  df2ndres  32797  nn0disj01  32911  dfdec100  32922  decdiv10  32974  dpmul100  32975  dpmul1000  32977  dpexpp1  32986  dpadd2  32988  dpadd  32989  dpmul  32991  dpmul4  32992  threehalves  32993  xrge00  33093  xrge0mulgnn0  33094  cyc2fv1  33202  cyc3conja  33238  elrgspnlem4  33326  xrge0slmod  33431  opprqusplusg  33572  opprqusmulr  33574  selvply1rhmlemb  33703  extvfvcl  33720  2sqr3nconstr  33965  cos9thpiminplylem1  33966  cos9thpiminplylem5  33970  cos9thpinconstrlem2  33974  lmatfvlem  33999  xrge0iifcnv  34117  lmxrge0  34136  cnrrext  34194  qqtopn  34195  esumrnmpt2  34252  esumpfinvallem  34258  unelldsys  34342  ldgenpisyslem1  34347  measunl  34400  mbfmcst  34443  difelcarsg  34494  carsggect  34502  sibfof  34524  eulerpartlemmf  34559  fib2  34586  fib3  34587  fib4  34588  fib5  34589  fib6  34590  0rrv  34635  coinfliprv  34667  ballotlem2  34673  prodfzo03  34787  chtvalz  34813  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  kur14lem6  35439  kur14lem7  35440  cvmlift2lem12  35542  problem5  35897  quad3  35898  divcnvlin  35961  in-ax8  36452  bj-2upln1upl  37377  bj-rest0  37451  relowlssretop  37725  relowlpssretop  37726  1oequni2o  37730  curunc  37969  ptrest  37986  poimirlem16  38003  poimirlem30  38017  mblfinlem2  38025  ovoliunnfl  38029  voliunnfl  38031  itg2addnclem2  38039  ftc1anclem5  38064  ftc1anclem6  38065  sdc  38111  heiborlem3  38180  xrnresex  38796  dmxrncnvepres  38799  dvh4dimN  41939  12gcd5e1  42488  60gcd6e6  42489  60gcd7e1  42490  420gcd8e4  42491  lcmeprodgcdi  42492  lcmineqlem23  42536  sq3deccom12  42767  asin1half  42834  acos1half  42835  redvmptabs  42837  readvrec  42839  sn-it1ei  42914  sn-0tie0  42941  dnnumch1  43489  aomclem6  43504  areaquad  43661  naddov4  43828  unitadd  44639  seff  44753  sblpnf  44754  hashnzfz  44764  lhe4.4ex1a  44773  xrtgcntopre  45921  iccdifioo  45960  itgsin0pilem1  46393  stoweidlem13  46456  stoweidlem26  46469  fourierdlem62  46611  fourierdlem102  46651  fourierdlem114  46663  fourierswlem  46673  fouriersw  46674  sge0tsms  46823  meaiuninc  46924  cos5t  47342  fmtno4prmfac  48050  41prothprm  48097  ppivalnn4  48105  dfclnbgr4  48315  2zrngasgrp  48737  2zrngmsgrp  48744  tposres3  49371  eloppf  49623  setc1onsubc  50092  mvlraddi  50261  mvlrmuli  50267  i2linesi  50268