Theorem eqtr3i 2754

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  3eqtr3i  2760  3eqtr3ri  2761  unundi  4135  unundir  4136  inindi  4194  inindir  4195  dfin4  4237  difun1  4258  difabs  4262  notab  4273  dif0  4337  disjdifr  4432  difdifdir  4451  pwundif  4583  tpidm13  4716  intmin2  4935  iunxdif3  5054  univ  5406  iunxpconst  5704  rnresi  6035  rnresv  6162  cnvsn0  6171  resdmres  6193  coi2  6224  coires1  6225  dfdm2  6242  isarep2  6590  resasplit  6712  ssimaex  6928  fnreseql  7002  resfunexg  7171  mpompt  7483  caov31  7598  fvresex  7918  xpexgALT  7939  1st2val  7975  2nd2val  7976  cnvoprab  8018  fnsuppeq0  8148  ecopovtrn  8770  limensuci  9094  pwfilem  9243  r1sucg  9698  jech9.3  9743  rankbnd2  9798  djuin  9847  compss  10305  zorn2lem4  10428  iunfo  10468  cardf  10479  alephsuc3  10509  fpwwe2lem12  10571  rankcf  10706  halfnq  10905  addclprlem2  10946  mulgt0sr  11034  mul02lem2  11327  mul02  11328  addrid  11330  mvlladdi  11416  mvllmuli  11991  infrenegsup  12142  8th4div3  12378  halfpm6th  12380  nneo  12594  nummac  12670  numadd  12672  numaddc  12673  nummul1c  12674  decbin0  12765  rpsup  13804  resup  13805  om2uzrdg  13897  m1expcl2  14026  facnn  14216  fac0  14217  faclbnd4lem1  14234  4bc3eq4  14269  hasheq0  14304  f1oun2prg  14859  sqrt1  15213  sqrt4  15214  sqrt9  15215  rddif  15283  abs3lemi  15353  sumss2  15668  divcnvshft  15797  geo2sum2  15816  geomulcvg  15818  geoihalfsum  15824  risefall0lem  15968  bpoly2  15999  bpoly3  16000  sin0  16093  efival  16096  ef01bndlem  16128  cos2bnd  16132  sin4lt0  16139  flodddiv4  16361  2prm  16638  unbenlem  16855  dec5dvds  17011  modxai  17015  mod2xi  17016  mod2xnegi  17018  gcdi  17020  numexp2x  17025  decsplit  17029  setsid  17153  xrge0base  17546  mreexexlem3d  17587  oppchom  17656  2oppchomf  17665  isoval  17707  estrres  18080  oppchofcl  18201  oyoncl  18211  mvdco  19359  m1expaddsub  19412  psgn0fv0  19425  oppglsm  19556  dprd2da  19958  ring1  20230  opprsubg  20272  lsppratlem1  21089  pzriprnglem7  21429  zzngim  21494  cnmsgnsubg  21519  psgninv  21524  zrhpsgnmhm  21526  ply1basfvi  22158  coe1tm  22192  ply1coe  22218  comppfsc  23452  kgeni  23457  xkoinjcn  23607  ufprim  23829  metreslem  24283  retopbas  24681  cnfldms  24696  qdensere2  24718  xrsmopn  24734  metdscn2  24779  pcoass  24957  recvs  25079  zclmncvs  25081  iscmet3lem3  25223  cncms  25288  cnfldcusp  25290  resscdrg  25291  rrxprds  25322  ovoliunnul  25441  uniioombllem4  25520  vitalilem5  25546  mbfres  25578  ismbf3d  25588  i1fima  25612  i1fd  25615  itg2cnlem1  25695  itgss3  25749  ellimc2  25811  limccnp2  25826  cpnres  25872  lhop  25954  plyeq0  26149  plypf1  26150  sinhalfpilem  26405  sincos6thpi  26458  sincos3rdpi  26459  pige3ALT  26462  dfrelog  26507  logi  26529  logimul  26556  logneg2  26557  dvlog  26593  cxpsqrt  26645  ang180lem2  26753  ang180lem3  26754  ang180lem4  26755  quart1  26799  asin1  26837  atan0  26851  atanlogsublem  26858  atan1  26871  log2tlbnd  26888  log2ublem2  26890  log2ub  26892  basellem8  27031  cht2  27115  ppiub  27148  bposlem6  27233  bposlem8  27235  bposlem9  27236  lgsdir2lem3  27271  lgseisenlem1  27319  lgseisenlem2  27320  lgsquadlem1  27324  lgsquadlem2  27325  2lgsoddprmlem2  27353  chebbnd1  27416  negsbdaylem  28002  om2noseqrdg  28238  zseo  28349  istrkg3ld  28441  tgcgr4  28511  motplusg  28522  ax5seglem7  28915  ex-un  30403  ex-sqrt  30433  ipdirilem  30808  ipasslem10  30818  hisubcomi  31083  normlem0  31088  norm3difi  31126  norm3lem  31128  polid2i  31136  chdmj1i  31460  chjjdiri  31503  spansn0  31520  pjoml4i  31566  cmbr3i  31579  qlaxr3i  31615  honpcani  31804  honpncani  31806  lnopunilem1  31989  lnophmlem2  31996  lnfn0i  32021  pjbdlni  32128  pjclem1  32174  pjclem3  32176  pjci  32179  atomli  32361  atabs2i  32381  mddmdin0i  32410  imadifxp  32580  fnresin  32600  ofpreima2  32640  df1stres  32677  df2ndres  32678  nn0disj01  32793  dfdec100  32805  decdiv10  32866  dpmul100  32867  dpmul1000  32869  dpexpp1  32878  dpadd2  32880  dpadd  32881  dpmul  32883  dpmul4  32884  threehalves  32885  xrge00  32998  xrge0mulgnn0  32999  cyc2fv1  33093  cyc3conja  33129  elrgspnlem4  33212  xrge0slmod  33312  opprqusplusg  33453  opprqusmulr  33455  2sqr3nconstr  33764  cos9thpiminplylem1  33765  cos9thpiminplylem5  33769  cos9thpinconstrlem2  33773  lmatfvlem  33798  xrge0iifcnv  33916  lmxrge0  33935  cnrrext  33993  qqtopn  33994  esumrnmpt2  34051  esumpfinvallem  34057  unelldsys  34141  ldgenpisyslem1  34146  measunl  34199  mbfmcst  34243  difelcarsg  34294  carsggect  34302  sibfof  34324  eulerpartlemmf  34359  fib2  34386  fib3  34387  fib4  34388  fib5  34389  fib6  34390  0rrv  34435  coinfliprv  34467  ballotlem2  34473  prodfzo03  34587  chtvalz  34613  hgt750lemd  34632  hgt750lem  34635  hgt750lem2  34636  kur14lem6  35191  kur14lem7  35192  cvmlift2lem12  35294  problem5  35649  quad3  35650  divcnvlin  35713  in-ax8  36205  bj-2upln1upl  37005  bj-rest0  37074  relowlssretop  37344  relowlpssretop  37345  1oequni2o  37349  curunc  37589  ptrest  37606  poimirlem16  37623  poimirlem30  37637  mblfinlem2  37645  ovoliunnfl  37649  voliunnfl  37651  itg2addnclem2  37659  ftc1anclem5  37684  ftc1anclem6  37685  sdc  37731  heiborlem3  37800  xrnresex  38385  dmxrncnvepres  38388  dvh4dimN  41434  12gcd5e1  41984  60gcd6e6  41985  60gcd7e1  41986  420gcd8e4  41987  lcmeprodgcdi  41988  lcmineqlem23  42032  sq3deccom12  42271  asin1half  42338  acos1half  42339  redvmptabs  42341  readvrec  42343  sn-it1ei  42418  sn-0tie0  42432  dnnumch1  43026  aomclem6  43041  areaquad  43198  naddov4  43365  unitadd  44177  seff  44291  sblpnf  44292  hashnzfz  44302  lhe4.4ex1a  44311  xrtgcntopre  45467  iccdifioo  45506  itgsin0pilem1  45941  stoweidlem13  46004  stoweidlem26  46017  fourierdlem62  46159  fourierdlem102  46199  fourierdlem114  46211  fourierswlem  46221  fouriersw  46222  sge0tsms  46371  meaiuninc  46472  tworepnotupword  46877  fmtno4prmfac  47566  41prothprm  47613  dfclnbgr4  47818  2zrngasgrp  48227  2zrngmsgrp  48234  tposres3  48862  eloppf  49115  setc1onsubc  49584  mvlraddi  49753  mvlrmuli  49759  i2linesi  49760