Theorem eqtr3i 2788

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  3eqtr3i  2794  3eqtr3ri  2795  inindi  4134  inindir  4135  unundi  4177  unundir  4178  dfin4  4226  difun1  4247  difabs  4251  notab  4262  dif0  4330  difdifdir  4450  pwundif  4586  tpidm13  4719  intmin2  4940  iunxdif3  5060  univ  5426  iunxpconst  5731  resdmdfsn  6039  rnresi  6091  rnresv  6214  imadifssranOLD  6221  cnvsn0  6230  resdmres  6252  coi2  6286  coires1  6288  dfdm2  6308  isarep2  6659  resasplit  6782  ssimaex  7001  fnreseql  7078  resfunexg  7252  mpompt  7565  caov31  7682  fvresex  8006  xpexgALT  8027  1st2val  8063  2nd2val  8064  cnvoprab  8106  fnsuppeq0  8247  ecopovtrn  8879  limensuci  9210  pwfilem  9347  r1sucg  9813  jech9.3OLD  9860  rankbnd2  9923  djuin  10036  cardprcALT  10100  compss  10493  zorn2lem4  10616  iunfo  10662  cardf  10673  alephsuc3  10704  fpwwe2lem12  10766  rankcf  10901  halfnq  11100  addclprlem2  11141  mulgt0sr  11229  mul02lem2  11526  mul02  11527  addrid  11529  mvlladdi  11615  mvllmuli  12190  infrenegsup  12340  halfpm6th  12608  nneo  12823  nummac  12904  numadd  12906  numaddc  12907  nummul1c  12908  decbin0  13001  fz00m1  13719  rpsup  14046  resup  14047  om2uzrdg  14139  m1expcl2  14268  facnn  14460  fac0  14461  faclbnd4lem1  14478  4bc3eq4  14513  hasheq0  14548  f1oun2prg  15111  sqrt1  15481  sqrt4  15482  sqrt9  15483  rddif  15552  abs3lemi  15622  sumss2  15936  divcnvshft  16068  geo2sum2  16087  geomulcvg  16089  geoihalfsum  16095  bpoly2  16267  bpoly3  16268  sin0  16361  efival  16364  ef01bndlem  16396  cos2bnd  16400  sin4lt0  16407  flodddiv4  16629  2prm  16911  unbenlem  17130  dec5dvds  17286  modxai  17290  mod2xi  17291  mod2xnegi  17293  gcdi  17295  numexp2x  17300  decsplit  17304  setsid  17429  xrge0base  17829  mreexexlem3d  17870  oppchom  17939  2oppchomf  17948  isoval  17990  estrres  18363  oppchofcl  18484  oyoncl  18494  mvdco  19710  m1expaddsub  19763  psgn0fv0  19776  oppglsm  19907  dprd2da  20309  ring1  20592  opprsubg  20633  lsppratlem1  21476  pzriprnglem7  21848  zzngim  21913  cnmsgnsubg  21938  psgninv  21943  zrhpsgnmhm  21945  ply1basfvi  22613  coe1tm  22647  ply1coe  22671  comppfsc  23906  kgeni  23911  xkoinjcn  24061  ufprim  24283  metreslem  24736  retopbas  25134  cnfldms  25149  qdensere2  25171  xrsmopn  25187  metdscn2  25232  pcoass  25400  recvs  25522  zclmncvs  25524  iscmet3lem3  25666  cncms  25731  cnfldcusp  25733  resscdrg  25734  rrxprds  25765  ovoliunnul  25883  uniioombllem4  25962  vitalilem5  25988  mbfres  26020  ismbf3d  26030  i1fima  26054  i1fd  26057  itg2cnlem1  26137  itgss3  26190  ellimc2  26252  limccnp2  26267  cpnres  26312  lhop  26391  plyeq0  26585  plypf1  26586  sinhalfpilem  26849  sincos6thpi  26901  sincos3rdpi  26902  pige3ALT  26905  dfrelog  26950  logi  26972  logimul  26999  logneg2  27000  dvlog  27036  cxpsqrt  27088  ang180lem2  27195  ang180lem3  27196  ang180lem4  27197  quart1  27241  asin1  27279  atan0  27293  atanlogsublem  27300  atan1  27313  log2tlbnd  27330  log2ublem2  27332  log2ub  27334  cht2  27556  ppiub  27588  bposlem6  27673  bposlem8  27675  bposlem9  27676  lgsdir2lem3  27711  lgseisenlem1  27759  lgseisenlem2  27760  lgsquadlem1  27764  lgsquadlem2  27765  2lgsoddprmlem2  27793  chebbnd1  27856  negbdaylem  28499  om2noseqrdg  28747  zseo  28865  bdaypw2n0bndlem  28906  istrkg3ld  28980  tgcgr4  29051  motplusg  29062  ax5seglem7  29570  ex-un  31082  ex-sqrt  31112  ipdirilem  31488  ipasslem10  31498  hisubcomi  31763  normlem0  31768  norm3difi  31806  norm3lem  31808  polid2i  31816  chdmj1i  32140  chjjdiri  32183  spansn0  32200  pjoml4i  32246  cmbr3i  32259  qlaxr3i  32295  honpcani  32484  honpncani  32486  lnopunilem1  32669  lnophmlem2  32676  lnfn0i  32701  pjbdlni  32808  pjclem1  32854  pjclem3  32856  pjci  32859  atomli  33041  atabs2i  33061  mddmdin0i  33090  imadifxp  33293  fnresin  33316  ofpreima2  33358  df1stres  33394  df2ndres  33395  nn0disj01  33506  dfdec100  33517  decdiv10  33558  dpmul100  33559  dpmul1000  33561  dpexpp1  33570  dpadd2  33572  dpadd  33573  dpmul  33575  dpmul4  33576  threehalves  33577  xrge00  33674  xrge0mulgnn0  33675  cyc2fv1  33781  cyc3conja  33817  elrgspnlem4  33905  xrge0slmod  34013  opprqusplusg  34117  opprqusmulr  34119  selvply1rhmlemb  34262  extvfvcl  34279  2sqr3nconstr  34524  cos9thpiminplylem1  34525  cos9thpiminplylem5  34529  cos9thpinconstrlem2  34533  lmatfvlem  34558  xrge0iifcnv  34676  lmxrge0  34695  cnrrext  34753  qqtopn  34754  esumrnmpt2  34811  esumpfinvallem  34817  unelldsys  34902  ldgenpisyslem1  34907  measunl  34960  mbfmcst  35002  difelcarsg  35053  carsggect  35061  sibfof  35083  eulerpartlemmf  35118  fib2  35145  fib3  35146  fib4  35147  fib5  35148  fib6  35149  0rrv  35194  coinfliprv  35226  ballotlem2  35232  prodfzo03  35343  chtvalz  35369  hgt750lemd  35388  hgt750lem  35391  hgt750lem2  35392  1enumen  35848  kur14lem6  36184  kur14lem7  36185  cvmlift2lem12  36287  problem5  36642  quad3  36643  divcnvlin  36713  in-ax8  37228  bj-2upln1upl  38152  coss2b  38218  coidmid  38225  bj-rest0  38284  relowlssretop  38554  relowlpssretop  38555  1oequni2o  38559  curunc  38793  ptrest  38805  poimirlem16  38822  poimirlem30  38836  mblfinlem2  38844  ovoliunnfl  38848  voliunnfl  38850  itg2addnclem2  38858  ftc1anclem5  38883  ftc1anclem6  38884  sdc  38944  heiborlem3  39013  xrnresex  39627  dmxrncnvepres  39630  dvh4dimN  42770  12gcd5e1  43319  60gcd6e6  43320  60gcd7e1  43321  420gcd8e4  43322  lcmeprodgcdi  43323  25or6to4  43522  sq3deccom12  43613  asin1half  43674  acos1half  43675  redvmptabs  43677  readvrec  43679  sn-it1ei  43754  sn-0tie0  43781  dnnumch1  44317  aomclem6  44327  areaquad  44479  naddov4  44646  unitadd  45456  seff  45554  sblpnf  45555  hashnzfz  45565  lhe4.4ex1a  45574  xrtgcntopre  46761  iccdifioo  46800  itgsin0pilem1  47233  stoweidlem13  47296  stoweidlem26  47309  fourierdlem62  47451  fourierdlem102  47491  fourierdlem114  47503  fourierswlem  47513  fouriersw  47514  sge0tsms  47663  meaiuninc  47764  cos5t  48198  goldpolyfactor  48200  goldratval  48209  fmtno4prmfac  48930  41prothprm  48977  ppivalnn4  48985  dfclnbgr4  49195  2zrngasgrp  49616  2zrngmsgrp  49623  bru4  49752  bru3val  49753  bru3sq  49755  tposres3  50325  eloppf  50580  setc1onsubc  51071  dvsec  51284  dvcsc  51285  dvcot  51286  mvlraddi  51295  mvlrmuli  51301  i2linesi  51302  veroquadmodzerod  51412