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  4127  unundir  4128  inindi  4186  inindir  4187  dfin4  4229  difun1  4250  difabs  4254  notab  4265  dif0  4329  disjdifr  4424  difdifdir  4443  pwundif  4575  tpidm13  4708  intmin2  4925  iunxdif3  5044  univ  5394  iunxpconst  5692  rnresi  6026  rnresv  6150  cnvsn0  6159  resdmres  6181  coi2  6212  coires1  6213  dfdm2  6229  isarep2  6572  resasplit  6694  ssimaex  6908  fnreseql  6982  resfunexg  7151  mpompt  7463  caov31  7578  fvresex  7895  xpexgALT  7916  1st2val  7952  2nd2val  7953  cnvoprab  7995  fnsuppeq0  8125  ecopovtrn  8747  limensuci  9070  pwfilem  9207  r1sucg  9665  jech9.3  9710  rankbnd2  9765  djuin  9814  compss  10270  zorn2lem4  10393  iunfo  10433  cardf  10444  alephsuc3  10474  fpwwe2lem12  10536  rankcf  10671  halfnq  10870  addclprlem2  10911  mulgt0sr  10999  mul02lem2  11293  mul02  11294  addrid  11296  mvlladdi  11382  mvllmuli  11957  infrenegsup  12108  8th4div3  12344  halfpm6th  12346  nneo  12560  nummac  12636  numadd  12638  numaddc  12639  nummul1c  12640  decbin0  12731  rpsup  13770  resup  13771  om2uzrdg  13863  m1expcl2  13992  facnn  14182  fac0  14183  faclbnd4lem1  14200  4bc3eq4  14235  hasheq0  14270  f1oun2prg  14824  sqrt1  15178  sqrt4  15179  sqrt9  15180  rddif  15248  abs3lemi  15318  sumss2  15633  divcnvshft  15762  geo2sum2  15781  geomulcvg  15783  geoihalfsum  15789  risefall0lem  15933  bpoly2  15964  bpoly3  15965  sin0  16058  efival  16061  ef01bndlem  16093  cos2bnd  16097  sin4lt0  16104  flodddiv4  16326  2prm  16603  unbenlem  16820  dec5dvds  16976  modxai  16980  mod2xi  16981  mod2xnegi  16983  gcdi  16985  numexp2x  16990  decsplit  16994  setsid  17118  xrge0base  17511  mreexexlem3d  17552  oppchom  17621  2oppchomf  17630  isoval  17672  estrres  18045  oppchofcl  18166  oyoncl  18176  mvdco  19324  m1expaddsub  19377  psgn0fv0  19390  oppglsm  19521  dprd2da  19923  ring1  20195  opprsubg  20237  lsppratlem1  21054  pzriprnglem7  21394  zzngim  21459  cnmsgnsubg  21484  psgninv  21489  zrhpsgnmhm  21491  ply1basfvi  22123  coe1tm  22157  ply1coe  22183  comppfsc  23417  kgeni  23422  xkoinjcn  23572  ufprim  23794  metreslem  24248  retopbas  24646  cnfldms  24661  qdensere2  24683  xrsmopn  24699  metdscn2  24744  pcoass  24922  recvs  25044  zclmncvs  25046  iscmet3lem3  25188  cncms  25253  cnfldcusp  25255  resscdrg  25256  rrxprds  25287  ovoliunnul  25406  uniioombllem4  25485  vitalilem5  25511  mbfres  25543  ismbf3d  25553  i1fima  25577  i1fd  25580  itg2cnlem1  25660  itgss3  25714  ellimc2  25776  limccnp2  25791  cpnres  25837  lhop  25919  plyeq0  26114  plypf1  26115  sinhalfpilem  26370  sincos6thpi  26423  sincos3rdpi  26424  pige3ALT  26427  dfrelog  26472  logi  26494  logimul  26521  logneg2  26522  dvlog  26558  cxpsqrt  26610  ang180lem2  26718  ang180lem3  26719  ang180lem4  26720  quart1  26764  asin1  26802  atan0  26816  atanlogsublem  26823  atan1  26836  log2tlbnd  26853  log2ublem2  26855  log2ub  26857  basellem8  26996  cht2  27080  ppiub  27113  bposlem6  27198  bposlem8  27200  bposlem9  27201  lgsdir2lem3  27236  lgseisenlem1  27284  lgseisenlem2  27285  lgsquadlem1  27289  lgsquadlem2  27290  2lgsoddprmlem2  27318  chebbnd1  27381  negsbdaylem  27967  om2noseqrdg  28203  zseo  28314  istrkg3ld  28406  tgcgr4  28476  motplusg  28487  ax5seglem7  28880  ex-un  30368  ex-sqrt  30398  ipdirilem  30773  ipasslem10  30783  hisubcomi  31048  normlem0  31053  norm3difi  31091  norm3lem  31093  polid2i  31101  chdmj1i  31425  chjjdiri  31468  spansn0  31485  pjoml4i  31531  cmbr3i  31544  qlaxr3i  31580  honpcani  31769  honpncani  31771  lnopunilem1  31954  lnophmlem2  31961  lnfn0i  31986  pjbdlni  32093  pjclem1  32139  pjclem3  32141  pjci  32144  atomli  32326  atabs2i  32346  mddmdin0i  32375  imadifxp  32545  fnresin  32568  ofpreima2  32609  df1stres  32646  df2ndres  32647  nn0disj01  32763  dfdec100  32775  decdiv10  32836  dpmul100  32837  dpmul1000  32839  dpexpp1  32848  dpadd2  32850  dpadd  32851  dpmul  32853  dpmul4  32854  threehalves  32855  xrge00  32968  xrge0mulgnn0  32969  cyc2fv1  33063  cyc3conja  33099  elrgspnlem4  33185  xrge0slmod  33285  opprqusplusg  33426  opprqusmulr  33428  2sqr3nconstr  33748  cos9thpiminplylem1  33749  cos9thpiminplylem5  33753  cos9thpinconstrlem2  33757  lmatfvlem  33782  xrge0iifcnv  33900  lmxrge0  33919  cnrrext  33977  qqtopn  33978  esumrnmpt2  34035  esumpfinvallem  34041  unelldsys  34125  ldgenpisyslem1  34130  measunl  34183  mbfmcst  34227  difelcarsg  34278  carsggect  34286  sibfof  34308  eulerpartlemmf  34343  fib2  34370  fib3  34371  fib4  34372  fib5  34373  fib6  34374  0rrv  34419  coinfliprv  34451  ballotlem2  34457  prodfzo03  34571  chtvalz  34597  hgt750lemd  34616  hgt750lem  34619  hgt750lem2  34620  kur14lem6  35184  kur14lem7  35185  cvmlift2lem12  35287  problem5  35642  quad3  35643  divcnvlin  35706  in-ax8  36198  bj-2upln1upl  36998  bj-rest0  37067  relowlssretop  37337  relowlpssretop  37338  1oequni2o  37342  curunc  37582  ptrest  37599  poimirlem16  37616  poimirlem30  37630  mblfinlem2  37638  ovoliunnfl  37642  voliunnfl  37644  itg2addnclem2  37652  ftc1anclem5  37677  ftc1anclem6  37678  sdc  37724  heiborlem3  37793  xrnresex  38378  dmxrncnvepres  38381  dvh4dimN  41426  12gcd5e1  41976  60gcd6e6  41977  60gcd7e1  41978  420gcd8e4  41979  lcmeprodgcdi  41980  lcmineqlem23  42024  sq3deccom12  42263  asin1half  42330  acos1half  42331  redvmptabs  42333  readvrec  42335  sn-it1ei  42410  sn-0tie0  42424  dnnumch1  43017  aomclem6  43032  areaquad  43189  naddov4  43356  unitadd  44168  seff  44282  sblpnf  44283  hashnzfz  44293  lhe4.4ex1a  44302  xrtgcntopre  45457  iccdifioo  45496  itgsin0pilem1  45931  stoweidlem13  45994  stoweidlem26  46007  fourierdlem62  46149  fourierdlem102  46189  fourierdlem114  46201  fourierswlem  46211  fouriersw  46212  sge0tsms  46361  meaiuninc  46462  tworepnotupword  46867  fmtno4prmfac  47556  41prothprm  47603  dfclnbgr4  47808  2zrngasgrp  48230  2zrngmsgrp  48237  tposres3  48865  eloppf  49118  setc1onsubc  49587  mvlraddi  49756  mvlrmuli  49762  i2linesi  49763