Theorem eqtr3i 2757

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

Syntax hints:   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719

This theorem is referenced by:  3eqtr3i  2763  3eqtr3ri  2764  rabrabiOLD  3451  unundi  4166  unundir  4167  inindi  4222  inindir  4223  dfin4  4263  difun1  4285  difabs  4289  notab  4300  dif0  4368  disjdifr  4468  difdifdir  4487  pwundif  4622  tpidm13  4756  intmin2  4973  iunxdif3  5092  univ  5447  iunxpconst  5744  rnresi  6072  rnresv  6199  cnvsn0  6208  resdmres  6230  coi2  6261  coires1  6262  dfdm2  6279  isarep2  6638  resasplit  6761  ssimaex  6977  fnreseql  7051  resfunexg  7221  mpompt  7528  caov31  7644  fvresex  7957  xpexgALT  7979  1st2val  8015  2nd2val  8016  cnvoprab  8058  fnsuppeq0  8190  ecopovtrn  8830  limensuci  9169  pwfilem  9193  pssnnOLD  9281  r1sucg  9784  jech9.3  9829  rankbnd2  9884  djuin  9933  compss  10391  zorn2lem4  10514  iunfo  10554  cardf  10565  alephsuc3  10595  fpwwe2lem12  10657  rankcf  10792  halfnq  10991  addclprlem2  11032  mulgt0sr  11120  mul02lem2  11413  mul02  11414  addrid  11416  mvlladdi  11500  mvllmuli  12069  infrenegsup  12219  8th4div3  12454  nneo  12668  nummac  12744  numadd  12746  numaddc  12747  nummul1c  12748  decbin0  12839  rpsup  13855  resup  13856  om2uzrdg  13945  m1expcl2  14074  facnn  14258  fac0  14259  faclbnd4lem1  14276  4bc3eq4  14311  hasheq0  14346  f1oun2prg  14892  sqrt1  15242  sqrt4  15243  sqrt9  15244  rddif  15311  abs3lemi  15381  sumss2  15696  divcnvshft  15825  geo2sum2  15844  geomulcvg  15846  geoihalfsum  15852  risefall0lem  15994  bpoly2  16025  bpoly3  16026  sin0  16117  efival  16120  ef01bndlem  16152  cos2bnd  16156  sin4lt0  16163  flodddiv4  16381  2prm  16654  unbenlem  16868  dec5dvds  17024  modxai  17028  mod2xi  17029  mod2xnegi  17031  gcdi  17033  numexp2x  17039  decsplit  17043  setsid  17168  mreexexlem3d  17617  oppchom  17687  2oppchomf  17697  isoval  17739  estrres  18121  oppchofcl  18243  oyoncl  18253  mvdco  19391  m1expaddsub  19444  psgn0fv0  19457  oppglsm  19588  dprd2da  19990  ring1  20235  opprsubg  20280  lsppratlem1  21024  pzriprnglem7  21400  zzngim  21473  cnmsgnsubg  21496  psgninv  21501  zrhpsgnmhm  21503  ply1basfvi  22146  coe1tm  22179  ply1coe  22204  comppfsc  23423  kgeni  23428  xkoinjcn  23578  ufprim  23800  metreslem  24255  retopbas  24664  cnfldms  24679  qdensere2  24700  xrsmopn  24715  metdscn2  24760  pcoass  24938  recvs  25060  recvsOLD  25061  zclmncvs  25063  iscmet3lem3  25205  cncms  25270  cnfldcusp  25272  resscdrg  25273  rrxprds  25304  ovoliunnul  25423  uniioombllem4  25502  vitalilem5  25528  mbfres  25560  ismbf3d  25570  i1fima  25594  i1fd  25597  itg2cnlem1  25678  itgss3  25731  ellimc2  25793  limccnp2  25808  cpnres  25854  lhop  25936  plyeq0  26132  plypf1  26133  sinhalfpilem  26385  sincos6thpi  26437  sincos3rdpi  26438  pige3ALT  26441  dfrelog  26486  logi  26508  logimul  26535  logneg2  26536  dvlog  26572  cxpsqrt  26624  ang180lem2  26729  ang180lem3  26730  ang180lem4  26731  quart1  26775  asin1  26813  atan0  26827  atanlogsublem  26834  atan1  26847  log2tlbnd  26864  log2ublem2  26866  log2ub  26868  basellem8  27007  cht2  27091  ppiub  27124  bposlem6  27209  bposlem8  27211  bposlem9  27212  lgsdir2lem3  27247  lgseisenlem1  27295  lgseisenlem2  27296  lgsquadlem1  27300  lgsquadlem2  27301  2lgsoddprmlem2  27329  chebbnd1  27392  negsbdaylem  27955  om2noseqrdg  28164  istrkg3ld  28252  tgcgr4  28322  motplusg  28333  ax5seglem7  28733  ex-un  30221  ex-sqrt  30251  ipdirilem  30626  ipasslem10  30636  hisubcomi  30901  normlem0  30906  norm3difi  30944  norm3lem  30946  polid2i  30954  chdmj1i  31278  chjjdiri  31321  spansn0  31338  pjoml4i  31384  cmbr3i  31397  qlaxr3i  31433  honpcani  31622  honpncani  31624  lnopunilem1  31807  lnophmlem2  31814  lnfn0i  31839  pjbdlni  31946  pjclem1  31992  pjclem3  31994  pjci  31997  atomli  32179  atabs2i  32199  mddmdin0i  32228  imadifxp  32376  fnresin  32394  ofpreima2  32435  df1stres  32467  df2ndres  32468  cnvoprabOLD  32486  dfdec100  32575  decdiv10  32601  dpmul100  32602  dpmul1000  32604  dpexpp1  32613  dpadd2  32615  dpadd  32616  dpmul  32618  dpmul4  32619  threehalves  32620  xrge0base  32723  xrge00  32724  xrge0mulgnn0  32727  cyc2fv1  32820  cyc3conja  32856  xrge0slmod  33000  opprqusplusg  33136  opprqusmulr  33138  lmatfvlem  33352  xrge0iifcnv  33470  lmxrge0  33489  cnrrext  33547  qqtopn  33548  esumrnmpt2  33623  esumpfinvallem  33629  unelldsys  33713  ldgenpisyslem1  33718  measunl  33771  mbfmcst  33815  difelcarsg  33866  carsggect  33874  sibfof  33896  eulerpartlemmf  33931  fib2  33958  fib3  33959  fib4  33960  fib5  33961  fib6  33962  0rrv  34007  coinfliprv  34038  ballotlem2  34044  prodfzo03  34171  chtvalz  34197  hgt750lemd  34216  hgt750lem  34219  hgt750lem2  34220  kur14lem6  34757  kur14lem7  34758  cvmlift2lem12  34860  problem5  35209  quad3  35210  divcnvlin  35263  bj-2upln1upl  36439  bj-rest0  36508  relowlssretop  36778  relowlpssretop  36779  1oequni2o  36783  curunc  37010  ptrest  37027  poimirlem16  37044  poimirlem30  37058  mblfinlem2  37066  ovoliunnfl  37070  voliunnfl  37072  itg2addnclem2  37080  ftc1anclem5  37105  ftc1anclem6  37106  sdc  37152  heiborlem3  37221  xrnresex  37815  dvh4dimN  40857  12gcd5e1  41411  60gcd6e6  41412  60gcd7e1  41413  420gcd8e4  41414  lcmeprodgcdi  41415  lcmineqlem23  41459  sq3deccom12  41786  sn-it1ei  41913  sn-0tie0  41916  sn-inelr  41942  acos1half  42019  dnnumch1  42390  aomclem6  42405  areaquad  42567  naddov4  42735  unitadd  43548  seff  43669  sblpnf  43670  hashnzfz  43680  lhe4.4ex1a  43689  xrtgcntopre  44784  iccdifioo  44823  itgsin0pilem1  45261  stoweidlem13  45324  stoweidlem26  45337  fourierdlem62  45479  fourierdlem102  45519  fourierdlem114  45531  fourierswlem  45541  fouriersw  45542  sge0tsms  45691  meaiuninc  45792  tworepnotupword  46195  fmtno4prmfac  46835  41prothprm  46882  2zrngasgrp  47231  2zrngmsgrp  47238  mvlraddi  48126  mvlrmuli  48133  i2linesi  48134