Theorem eqtr3i 2770

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  3eqtr3i  2776  3eqtr3ri  2777  rabrabiOLD  3469  unundi  4199  unundir  4200  inindi  4256  inindir  4257  dfin4  4297  difun1  4318  difabs  4322  notab  4333  dif0  4400  disjdifr  4496  difdifdir  4515  pwundif  4646  tpidm13  4781  intmin2  4999  iunxdif3  5118  univ  5471  iunxpconst  5772  rnresi  6104  rnresv  6232  cnvsn0  6241  resdmres  6263  coi2  6294  coires1  6295  dfdm2  6312  isarep2  6669  resasplit  6791  ssimaex  7007  fnreseql  7081  resfunexg  7252  mpompt  7564  caov31  7679  fvresex  8000  xpexgALT  8022  1st2val  8058  2nd2val  8059  cnvoprab  8101  fnsuppeq0  8233  ecopovtrn  8878  limensuci  9219  pwfilem  9384  r1sucg  9838  jech9.3  9883  rankbnd2  9938  djuin  9987  compss  10445  zorn2lem4  10568  iunfo  10608  cardf  10619  alephsuc3  10649  fpwwe2lem12  10711  rankcf  10846  halfnq  11045  addclprlem2  11086  mulgt0sr  11174  mul02lem2  11467  mul02  11468  addrid  11470  mvlladdi  11554  mvllmuli  12127  infrenegsup  12278  8th4div3  12513  nneo  12727  nummac  12803  numadd  12805  numaddc  12806  nummul1c  12807  decbin0  12898  rpsup  13917  resup  13918  om2uzrdg  14007  m1expcl2  14136  facnn  14324  fac0  14325  faclbnd4lem1  14342  4bc3eq4  14377  hasheq0  14412  f1oun2prg  14966  sqrt1  15320  sqrt4  15321  sqrt9  15322  rddif  15389  abs3lemi  15459  sumss2  15774  divcnvshft  15903  geo2sum2  15922  geomulcvg  15924  geoihalfsum  15930  risefall0lem  16074  bpoly2  16105  bpoly3  16106  sin0  16197  efival  16200  ef01bndlem  16232  cos2bnd  16236  sin4lt0  16243  flodddiv4  16461  2prm  16739  unbenlem  16955  dec5dvds  17111  modxai  17115  mod2xi  17116  mod2xnegi  17118  gcdi  17120  numexp2x  17126  decsplit  17130  setsid  17255  mreexexlem3d  17704  oppchom  17774  2oppchomf  17784  isoval  17826  estrres  18208  oppchofcl  18330  oyoncl  18340  mvdco  19487  m1expaddsub  19540  psgn0fv0  19553  oppglsm  19684  dprd2da  20086  ring1  20333  opprsubg  20378  lsppratlem1  21172  pzriprnglem7  21521  zzngim  21594  cnmsgnsubg  21618  psgninv  21623  zrhpsgnmhm  21625  ply1basfvi  22263  coe1tm  22297  ply1coe  22323  comppfsc  23561  kgeni  23566  xkoinjcn  23716  ufprim  23938  metreslem  24393  retopbas  24802  cnfldms  24817  qdensere2  24838  xrsmopn  24853  metdscn2  24898  pcoass  25076  recvs  25198  recvsOLD  25199  zclmncvs  25201  iscmet3lem3  25343  cncms  25408  cnfldcusp  25410  resscdrg  25411  rrxprds  25442  ovoliunnul  25561  uniioombllem4  25640  vitalilem5  25666  mbfres  25698  ismbf3d  25708  i1fima  25732  i1fd  25735  itg2cnlem1  25816  itgss3  25870  ellimc2  25932  limccnp2  25947  cpnres  25993  lhop  26075  plyeq0  26270  plypf1  26271  sinhalfpilem  26523  sincos6thpi  26576  sincos3rdpi  26577  pige3ALT  26580  dfrelog  26625  logi  26647  logimul  26674  logneg2  26675  dvlog  26711  cxpsqrt  26763  ang180lem2  26871  ang180lem3  26872  ang180lem4  26873  quart1  26917  asin1  26955  atan0  26969  atanlogsublem  26976  atan1  26989  log2tlbnd  27006  log2ublem2  27008  log2ub  27010  basellem8  27149  cht2  27233  ppiub  27266  bposlem6  27351  bposlem8  27353  bposlem9  27354  lgsdir2lem3  27389  lgseisenlem1  27437  lgseisenlem2  27438  lgsquadlem1  27442  lgsquadlem2  27443  2lgsoddprmlem2  27471  chebbnd1  27534  negsbdaylem  28106  om2noseqrdg  28328  zseo  28424  istrkg3ld  28487  tgcgr4  28557  motplusg  28568  ax5seglem7  28968  ex-un  30456  ex-sqrt  30486  ipdirilem  30861  ipasslem10  30871  hisubcomi  31136  normlem0  31141  norm3difi  31179  norm3lem  31181  polid2i  31189  chdmj1i  31513  chjjdiri  31556  spansn0  31573  pjoml4i  31619  cmbr3i  31632  qlaxr3i  31668  honpcani  31857  honpncani  31859  lnopunilem1  32042  lnophmlem2  32049  lnfn0i  32074  pjbdlni  32181  pjclem1  32227  pjclem3  32229  pjci  32232  atomli  32414  atabs2i  32434  mddmdin0i  32463  imadifxp  32623  fnresin  32645  ofpreima2  32684  df1stres  32715  df2ndres  32716  cnvoprabOLD  32734  nn0disj01  32822  dfdec100  32834  decdiv10  32860  dpmul100  32861  dpmul1000  32863  dpexpp1  32872  dpadd2  32874  dpadd  32875  dpmul  32877  dpmul4  32878  threehalves  32879  xrge0base  32997  xrge00  32998  xrge0mulgnn0  33001  cyc2fv1  33114  cyc3conja  33150  xrge0slmod  33341  opprqusplusg  33482  opprqusmulr  33484  lmatfvlem  33761  xrge0iifcnv  33879  lmxrge0  33898  cnrrext  33956  qqtopn  33957  esumrnmpt2  34032  esumpfinvallem  34038  unelldsys  34122  ldgenpisyslem1  34127  measunl  34180  mbfmcst  34224  difelcarsg  34275  carsggect  34283  sibfof  34305  eulerpartlemmf  34340  fib2  34367  fib3  34368  fib4  34369  fib5  34370  fib6  34371  0rrv  34416  coinfliprv  34447  ballotlem2  34453  prodfzo03  34580  chtvalz  34606  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  kur14lem6  35179  kur14lem7  35180  cvmlift2lem12  35282  problem5  35637  quad3  35638  divcnvlin  35695  in-ax8  36190  bj-2upln1upl  36990  bj-rest0  37059  relowlssretop  37329  relowlpssretop  37330  1oequni2o  37334  curunc  37562  ptrest  37579  poimirlem16  37596  poimirlem30  37610  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  itg2addnclem2  37632  ftc1anclem5  37657  ftc1anclem6  37658  sdc  37704  heiborlem3  37773  xrnresex  38362  dvh4dimN  41404  12gcd5e1  41960  60gcd6e6  41961  60gcd7e1  41962  420gcd8e4  41963  lcmeprodgcdi  41964  lcmineqlem23  42008  sq3deccom12  42279  asin1half  42339  acos1half  42340  sn-it1ei  42412  sn-0tie0  42415  sn-inelr  42443  dnnumch1  43001  aomclem6  43016  areaquad  43177  naddov4  43345  unitadd  44157  seff  44278  sblpnf  44279  hashnzfz  44289  lhe4.4ex1a  44298  xrtgcntopre  45394  iccdifioo  45433  itgsin0pilem1  45871  stoweidlem13  45934  stoweidlem26  45947  fourierdlem62  46089  fourierdlem102  46129  fourierdlem114  46141  fourierswlem  46151  fouriersw  46152  sge0tsms  46301  meaiuninc  46402  tworepnotupword  46805  fmtno4prmfac  47446  41prothprm  47493  dfclnbgr4  47698  2zrngasgrp  47969  2zrngmsgrp  47976  mvlraddi  48864  mvlrmuli  48871  i2linesi  48872