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  4106  unundir  4107  inindi  4164  inindir  4165  dfin4  4207  difun1  4228  difabs  4232  notab  4243  dif0  4307  difdifdir  4420  pwundif  4554  tpidm13  4689  intmin2  4906  iunxdif3  5025  univ  5391  iunxpconst  5692  rnresi  6028  rnresv  6153  cnvsn0  6162  resdmres  6184  coi2  6216  coires1  6217  dfdm2  6233  isarep2  6576  resasplit  6698  ssimaex  6913  fnreseql  6990  resfunexg  7160  mpompt  7471  caov31  7586  fvresex  7903  xpexgALT  7924  1st2val  7960  2nd2val  7961  cnvoprab  8003  fnsuppeq0  8133  ecopovtrn  8758  limensuci  9082  pwfilem  9219  r1sucg  9685  jech9.3  9730  rankbnd2  9785  djuin  9834  compss  10290  zorn2lem4  10413  iunfo  10453  cardf  10464  alephsuc3  10495  fpwwe2lem12  10557  rankcf  10692  halfnq  10891  addclprlem2  10932  mulgt0sr  11020  mul02lem2  11315  mul02  11316  addrid  11318  mvlladdi  11404  mvllmuli  11980  infrenegsup  12131  8th4div3  12389  halfpm6th  12391  nneo  12605  nummac  12681  numadd  12683  numaddc  12684  nummul1c  12685  decbin0  12776  rpsup  13817  resup  13818  om2uzrdg  13910  m1expcl2  14039  facnn  14229  fac0  14230  faclbnd4lem1  14247  4bc3eq4  14282  hasheq0  14317  f1oun2prg  14871  sqrt1  15225  sqrt4  15226  sqrt9  15227  rddif  15295  abs3lemi  15365  sumss2  15680  divcnvshft  15812  geo2sum2  15831  geomulcvg  15833  geoihalfsum  15839  risefall0lem  15983  bpoly2  16014  bpoly3  16015  sin0  16108  efival  16111  ef01bndlem  16143  cos2bnd  16147  sin4lt0  16154  flodddiv4  16376  2prm  16653  unbenlem  16871  dec5dvds  17027  modxai  17031  mod2xi  17032  mod2xnegi  17034  gcdi  17036  numexp2x  17041  decsplit  17045  setsid  17169  xrge0base  17563  mreexexlem3d  17604  oppchom  17673  2oppchomf  17682  isoval  17724  estrres  18097  oppchofcl  18218  oyoncl  18228  mvdco  19412  m1expaddsub  19465  psgn0fv0  19478  oppglsm  19609  dprd2da  20011  ring1  20283  opprsubg  20324  lsppratlem1  21141  pzriprnglem7  21463  zzngim  21528  cnmsgnsubg  21553  psgninv  21558  zrhpsgnmhm  21560  ply1basfvi  22226  coe1tm  22260  ply1coe  22285  comppfsc  23516  kgeni  23521  xkoinjcn  23671  ufprim  23893  metreslem  24346  retopbas  24744  cnfldms  24759  qdensere2  24781  xrsmopn  24797  metdscn2  24842  pcoass  25010  recvs  25132  zclmncvs  25134  iscmet3lem3  25276  cncms  25341  cnfldcusp  25343  resscdrg  25344  rrxprds  25375  ovoliunnul  25493  uniioombllem4  25572  vitalilem5  25598  mbfres  25630  ismbf3d  25640  i1fima  25664  i1fd  25667  itg2cnlem1  25747  itgss3  25801  ellimc2  25863  limccnp2  25878  cpnres  25923  lhop  26002  plyeq0  26195  plypf1  26196  sinhalfpilem  26446  sincos6thpi  26499  sincos3rdpi  26500  pige3ALT  26503  dfrelog  26548  logi  26570  logimul  26597  logneg2  26598  dvlog  26634  cxpsqrt  26686  ang180lem2  26793  ang180lem3  26794  ang180lem4  26795  quart1  26839  asin1  26877  atan0  26891  atanlogsublem  26898  atan1  26911  log2tlbnd  26928  log2ublem2  26930  log2ub  26932  basellem8  27070  cht2  27154  ppiub  27186  bposlem6  27271  bposlem8  27273  bposlem9  27274  lgsdir2lem3  27309  lgseisenlem1  27357  lgseisenlem2  27358  lgsquadlem1  27362  lgsquadlem2  27363  2lgsoddprmlem2  27391  chebbnd1  27454  negbdaylem  28067  om2noseqrdg  28315  zseo  28433  bdaypw2n0bndlem  28474  istrkg3ld  28548  tgcgr4  28618  motplusg  28629  ax5seglem7  29023  ex-un  30513  ex-sqrt  30543  ipdirilem  30919  ipasslem10  30929  hisubcomi  31194  normlem0  31199  norm3difi  31237  norm3lem  31239  polid2i  31247  chdmj1i  31571  chjjdiri  31614  spansn0  31631  pjoml4i  31677  cmbr3i  31690  qlaxr3i  31726  honpcani  31915  honpncani  31917  lnopunilem1  32100  lnophmlem2  32107  lnfn0i  32132  pjbdlni  32239  pjclem1  32285  pjclem3  32287  pjci  32290  atomli  32472  atabs2i  32492  mddmdin0i  32521  imadifxp  32691  fnresin  32717  ofpreima2  32759  df1stres  32797  df2ndres  32798  nn0disj01  32912  dfdec100  32923  decdiv10  32975  dpmul100  32976  dpmul1000  32978  dpexpp1  32987  dpadd2  32989  dpadd  32990  dpmul  32992  dpmul4  32993  threehalves  32994  xrge00  33094  xrge0mulgnn0  33095  cyc2fv1  33203  cyc3conja  33239  elrgspnlem4  33327  xrge0slmod  33432  opprqusplusg  33573  opprqusmulr  33575  selvply1rhmlemb  33712  extvfvcl  33729  2sqr3nconstr  33974  cos9thpiminplylem1  33975  cos9thpiminplylem5  33979  cos9thpinconstrlem2  33983  lmatfvlem  34008  xrge0iifcnv  34126  lmxrge0  34145  cnrrext  34203  qqtopn  34204  esumrnmpt2  34261  esumpfinvallem  34267  unelldsys  34351  ldgenpisyslem1  34356  measunl  34409  mbfmcst  34452  difelcarsg  34503  carsggect  34511  sibfof  34533  eulerpartlemmf  34568  fib2  34595  fib3  34596  fib4  34597  fib5  34598  fib6  34599  0rrv  34644  coinfliprv  34676  ballotlem2  34682  prodfzo03  34796  chtvalz  34822  hgt750lemd  34841  hgt750lem  34844  hgt750lem2  34845  kur14lem6  35448  kur14lem7  35449  cvmlift2lem12  35551  problem5  35906  quad3  35907  divcnvlin  35970  in-ax8  36461  bj-2upln1upl  37386  bj-rest0  37460  relowlssretop  37734  relowlpssretop  37735  1oequni2o  37739  curunc  37978  ptrest  37995  poimirlem16  38012  poimirlem30  38026  mblfinlem2  38034  ovoliunnfl  38038  voliunnfl  38040  itg2addnclem2  38048  ftc1anclem5  38073  ftc1anclem6  38074  sdc  38120  heiborlem3  38189  xrnresex  38805  dmxrncnvepres  38808  dvh4dimN  41948  12gcd5e1  42497  60gcd6e6  42498  60gcd7e1  42499  420gcd8e4  42500  lcmeprodgcdi  42501  lcmineqlem23  42545  sq3deccom12  42776  asin1half  42843  acos1half  42844  redvmptabs  42846  readvrec  42848  sn-it1ei  42923  sn-0tie0  42950  dnnumch1  43498  aomclem6  43513  areaquad  43670  naddov4  43837  unitadd  44648  seff  44762  sblpnf  44763  hashnzfz  44773  lhe4.4ex1a  44782  xrtgcntopre  45929  iccdifioo  45968  itgsin0pilem1  46401  stoweidlem13  46464  stoweidlem26  46477  fourierdlem62  46619  fourierdlem102  46659  fourierdlem114  46671  fourierswlem  46681  fouriersw  46682  sge0tsms  46831  meaiuninc  46932  cos5t  47350  fmtno4prmfac  48058  41prothprm  48105  ppivalnn4  48113  dfclnbgr4  48323  2zrngasgrp  48745  2zrngmsgrp  48752  tposres3  49379  eloppf  49631  setc1onsubc  50100  mvlraddi  50269  mvlrmuli  50275  i2linesi  50276