Theorem eqtr3i 2785

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  3eqtr3i  2791  3eqtr3ri  2792  inindi  4130  inindir  4131  unundi  4173  unundir  4174  dfin4  4222  difun1  4243  difabs  4247  notab  4258  dif0  4326  difdifdir  4446  pwundif  4582  tpidm13  4713  intmin2  4934  iunxdif3  5054  univ  5419  iunxpconst  5724  resdmdfsn  6023  rnresi  6075  rnresv  6198  imadifssranOLD  6205  cnvsn0  6214  resdmres  6236  coi2  6268  coires1  6269  dfdm2  6287  isarep2  6634  resasplit  6757  ssimaex  6975  fnreseql  7052  resfunexg  7225  mpompt  7538  caov31  7654  fvresex  7976  xpexgALT  7997  1st2val  8033  2nd2val  8034  cnvoprab  8075  fnsuppeq0  8216  ecopovtrn  8848  limensuci  9179  pwfilem  9316  r1sucg  9783  jech9.3OLD  9830  rankbnd2  9893  djuin  10006  compss  10461  zorn2lem4  10584  iunfo  10630  cardf  10641  alephsuc3  10672  fpwwe2lem12  10734  rankcf  10869  halfnq  11068  addclprlem2  11109  mulgt0sr  11197  mul02lem2  11494  mul02  11495  addrid  11497  mvlladdi  11583  mvllmuli  12157  infrenegsup  12307  halfpm6th  12575  nneo  12790  nummac  12871  numadd  12873  numaddc  12874  nummul1c  12875  decbin0  12968  fz00m1  13686  rpsup  14013  resup  14014  om2uzrdg  14106  m1expcl2  14235  facnn  14426  fac0  14427  faclbnd4lem1  14444  4bc3eq4  14479  hasheq0  14514  f1oun2prg  15077  sqrt1  15447  sqrt4  15448  sqrt9  15449  rddif  15517  abs3lemi  15587  sumss2  15901  divcnvshft  16033  geo2sum2  16052  geomulcvg  16054  geoihalfsum  16060  bpoly2  16232  bpoly3  16233  sin0  16326  efival  16329  ef01bndlem  16361  cos2bnd  16365  sin4lt0  16372  flodddiv4  16594  2prm  16876  unbenlem  17095  dec5dvds  17251  modxai  17255  mod2xi  17256  mod2xnegi  17258  gcdi  17260  numexp2x  17265  decsplit  17269  setsid  17394  xrge0base  17788  mreexexlem3d  17829  oppchom  17898  2oppchomf  17907  isoval  17949  estrres  18322  oppchofcl  18443  oyoncl  18453  mvdco  19668  m1expaddsub  19721  psgn0fv0  19734  oppglsm  19865  dprd2da  20267  ring1  20550  opprsubg  20591  lsppratlem1  21434  pzriprnglem7  21802  zzngim  21867  cnmsgnsubg  21892  psgninv  21897  zrhpsgnmhm  21899  ply1basfvi  22567  coe1tm  22601  ply1coe  22625  comppfsc  23860  kgeni  23865  xkoinjcn  24015  ufprim  24237  metreslem  24690  retopbas  25088  cnfldms  25103  qdensere2  25125  xrsmopn  25141  metdscn2  25186  pcoass  25354  recvs  25476  zclmncvs  25478  iscmet3lem3  25620  cncms  25685  cnfldcusp  25687  resscdrg  25688  rrxprds  25719  ovoliunnul  25837  uniioombllem4  25916  vitalilem5  25942  mbfres  25974  ismbf3d  25984  i1fima  26008  i1fd  26011  itg2cnlem1  26091  itgss3  26144  ellimc2  26206  limccnp2  26221  cpnres  26266  lhop  26345  plyeq0  26539  plypf1  26540  sinhalfpilem  26801  sincos6thpi  26853  sincos3rdpi  26854  pige3ALT  26857  dfrelog  26902  logi  26924  logimul  26951  logneg2  26952  dvlog  26988  cxpsqrt  27040  ang180lem2  27147  ang180lem3  27148  ang180lem4  27149  quart1  27193  asin1  27231  atan0  27245  atanlogsublem  27252  atan1  27265  log2tlbnd  27282  log2ublem2  27284  log2ub  27286  cht2  27508  ppiub  27540  bposlem6  27625  bposlem8  27627  bposlem9  27628  lgsdir2lem3  27663  lgseisenlem1  27711  lgseisenlem2  27712  lgsquadlem1  27716  lgsquadlem2  27717  2lgsoddprmlem2  27745  chebbnd1  27808  negbdaylem  28451  om2noseqrdg  28699  zseo  28817  bdaypw2n0bndlem  28858  istrkg3ld  28932  tgcgr4  29003  motplusg  29014  ax5seglem7  29522  ex-un  31034  ex-sqrt  31064  ipdirilem  31440  ipasslem10  31450  hisubcomi  31715  normlem0  31720  norm3difi  31758  norm3lem  31760  polid2i  31768  chdmj1i  32092  chjjdiri  32135  spansn0  32152  pjoml4i  32198  cmbr3i  32211  qlaxr3i  32247  honpcani  32436  honpncani  32438  lnopunilem1  32621  lnophmlem2  32628  lnfn0i  32653  pjbdlni  32760  pjclem1  32806  pjclem3  32808  pjci  32811  atomli  32993  atabs2i  33013  mddmdin0i  33042  imadifxp  33246  fnresin  33269  ofpreima2  33311  df1stres  33348  df2ndres  33349  nn0disj01  33460  dfdec100  33471  decdiv10  33512  dpmul100  33513  dpmul1000  33515  dpexpp1  33524  dpadd2  33526  dpadd  33527  dpmul  33529  dpmul4  33530  threehalves  33531  xrge00  33625  xrge0mulgnn0  33626  cyc2fv1  33732  cyc3conja  33768  elrgspnlem4  33856  xrge0slmod  33959  opprqusplusg  34063  opprqusmulr  34065  selvply1rhmlemb  34201  extvfvcl  34218  2sqr3nconstr  34463  cos9thpiminplylem1  34464  cos9thpiminplylem5  34468  cos9thpinconstrlem2  34472  lmatfvlem  34497  xrge0iifcnv  34615  lmxrge0  34634  cnrrext  34692  qqtopn  34693  esumrnmpt2  34750  esumpfinvallem  34756  unelldsys  34841  ldgenpisyslem1  34846  measunl  34899  mbfmcst  34941  difelcarsg  34992  carsggect  35000  sibfof  35022  eulerpartlemmf  35057  fib2  35084  fib3  35085  fib4  35086  fib5  35087  fib6  35088  0rrv  35133  coinfliprv  35165  ballotlem2  35171  prodfzo03  35282  chtvalz  35308  hgt750lemd  35327  hgt750lem  35330  hgt750lem2  35331  1enumen  35779  kur14lem6  36066  kur14lem7  36067  cvmlift2lem12  36169  problem5  36524  quad3  36525  cardprcALT  36555  divcnvlin  36594  in-ax8  37109  bj-2upln1upl  38033  bj-rest0  38122  relowlssretop  38395  relowlpssretop  38396  1oequni2o  38400  curunc  38634  ptrest  38646  poimirlem16  38663  poimirlem30  38677  mblfinlem2  38685  ovoliunnfl  38689  voliunnfl  38691  itg2addnclem2  38699  ftc1anclem5  38724  ftc1anclem6  38725  sdc  38787  heiborlem3  38856  xrnresex  39470  dmxrncnvepres  39473  dvh4dimN  42613  12gcd5e1  43162  60gcd6e6  43163  60gcd7e1  43164  420gcd8e4  43165  lcmeprodgcdi  43166  25or6to4  43365  sq3deccom12  43456  asin1half  43517  acos1half  43518  redvmptabs  43520  readvrec  43522  sn-it1ei  43597  sn-0tie0  43624  dnnumch1  44160  aomclem6  44170  areaquad  44327  naddov4  44494  unitadd  45304  seff  45402  sblpnf  45403  hashnzfz  45413  lhe4.4ex1a  45422  xrtgcntopre  46596  iccdifioo  46635  itgsin0pilem1  47068  stoweidlem13  47131  stoweidlem26  47144  fourierdlem62  47286  fourierdlem102  47326  fourierdlem114  47338  fourierswlem  47348  fouriersw  47349  sge0tsms  47498  meaiuninc  47599  cos5t  48033  goldpolyfactor  48035  goldratval  48044  fmtno4prmfac  48765  41prothprm  48812  ppivalnn4  48820  dfclnbgr4  49030  2zrngasgrp  49451  2zrngmsgrp  49458  tposres3  50102  eloppf  50357  setc1onsubc  50848  dvsec  51039  dvcsc  51040  dvcot  51041  mvlraddi  51050  mvlrmuli  51056  i2linesi  51057  veroquadmodzerod  51167