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  4139  unundir  4140  inindi  4198  inindir  4199  dfin4  4241  difun1  4262  difabs  4266  notab  4277  dif0  4341  disjdifr  4436  difdifdir  4455  pwundif  4587  tpidm13  4720  intmin2  4939  iunxdif3  5059  univ  5411  iunxpconst  5711  rnresi  6046  rnresv  6174  cnvsn0  6183  resdmres  6205  coi2  6236  coires1  6237  dfdm2  6254  isarep2  6608  resasplit  6730  ssimaex  6946  fnreseql  7020  resfunexg  7189  mpompt  7503  caov31  7618  fvresex  7938  xpexgALT  7960  1st2val  7996  2nd2val  7997  cnvoprab  8039  fnsuppeq0  8171  ecopovtrn  8793  limensuci  9117  pwfilem  9267  r1sucg  9722  jech9.3  9767  rankbnd2  9822  djuin  9871  compss  10329  zorn2lem4  10452  iunfo  10492  cardf  10503  alephsuc3  10533  fpwwe2lem12  10595  rankcf  10730  halfnq  10929  addclprlem2  10970  mulgt0sr  11058  mul02lem2  11351  mul02  11352  addrid  11354  mvlladdi  11440  mvllmuli  12015  infrenegsup  12166  8th4div3  12402  halfpm6th  12404  nneo  12618  nummac  12694  numadd  12696  numaddc  12697  nummul1c  12698  decbin0  12789  rpsup  13828  resup  13829  om2uzrdg  13921  m1expcl2  14050  facnn  14240  fac0  14241  faclbnd4lem1  14258  4bc3eq4  14293  hasheq0  14328  f1oun2prg  14883  sqrt1  15237  sqrt4  15238  sqrt9  15239  rddif  15307  abs3lemi  15377  sumss2  15692  divcnvshft  15821  geo2sum2  15840  geomulcvg  15842  geoihalfsum  15848  risefall0lem  15992  bpoly2  16023  bpoly3  16024  sin0  16117  efival  16120  ef01bndlem  16152  cos2bnd  16156  sin4lt0  16163  flodddiv4  16385  2prm  16662  unbenlem  16879  dec5dvds  17035  modxai  17039  mod2xi  17040  mod2xnegi  17042  gcdi  17044  numexp2x  17049  decsplit  17053  setsid  17177  mreexexlem3d  17607  oppchom  17676  2oppchomf  17685  isoval  17727  estrres  18100  oppchofcl  18221  oyoncl  18231  mvdco  19375  m1expaddsub  19428  psgn0fv0  19441  oppglsm  19572  dprd2da  19974  ring1  20219  opprsubg  20261  lsppratlem1  21057  pzriprnglem7  21397  zzngim  21462  cnmsgnsubg  21486  psgninv  21491  zrhpsgnmhm  21493  ply1basfvi  22125  coe1tm  22159  ply1coe  22185  comppfsc  23419  kgeni  23424  xkoinjcn  23574  ufprim  23796  metreslem  24250  retopbas  24648  cnfldms  24663  qdensere2  24685  xrsmopn  24701  metdscn2  24746  pcoass  24924  recvs  25046  zclmncvs  25048  iscmet3lem3  25190  cncms  25255  cnfldcusp  25257  resscdrg  25258  rrxprds  25289  ovoliunnul  25408  uniioombllem4  25487  vitalilem5  25513  mbfres  25545  ismbf3d  25555  i1fima  25579  i1fd  25582  itg2cnlem1  25662  itgss3  25716  ellimc2  25778  limccnp2  25793  cpnres  25839  lhop  25921  plyeq0  26116  plypf1  26117  sinhalfpilem  26372  sincos6thpi  26425  sincos3rdpi  26426  pige3ALT  26429  dfrelog  26474  logi  26496  logimul  26523  logneg2  26524  dvlog  26560  cxpsqrt  26612  ang180lem2  26720  ang180lem3  26721  ang180lem4  26722  quart1  26766  asin1  26804  atan0  26818  atanlogsublem  26825  atan1  26838  log2tlbnd  26855  log2ublem2  26857  log2ub  26859  basellem8  26998  cht2  27082  ppiub  27115  bposlem6  27200  bposlem8  27202  bposlem9  27203  lgsdir2lem3  27238  lgseisenlem1  27286  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  2lgsoddprmlem2  27320  chebbnd1  27383  negsbdaylem  27962  om2noseqrdg  28198  zseo  28308  istrkg3ld  28388  tgcgr4  28458  motplusg  28469  ax5seglem7  28862  ex-un  30353  ex-sqrt  30383  ipdirilem  30758  ipasslem10  30768  hisubcomi  31033  normlem0  31038  norm3difi  31076  norm3lem  31078  polid2i  31086  chdmj1i  31410  chjjdiri  31453  spansn0  31470  pjoml4i  31516  cmbr3i  31529  qlaxr3i  31565  honpcani  31754  honpncani  31756  lnopunilem1  31939  lnophmlem2  31946  lnfn0i  31971  pjbdlni  32078  pjclem1  32124  pjclem3  32126  pjci  32129  atomli  32311  atabs2i  32331  mddmdin0i  32360  imadifxp  32530  fnresin  32550  ofpreima2  32590  df1stres  32627  df2ndres  32628  nn0disj01  32743  dfdec100  32755  decdiv10  32816  dpmul100  32817  dpmul1000  32819  dpexpp1  32828  dpadd2  32830  dpadd  32831  dpmul  32833  dpmul4  32834  threehalves  32835  xrge0base  32952  xrge00  32953  xrge0mulgnn0  32956  cyc2fv1  33078  cyc3conja  33114  elrgspnlem4  33196  xrge0slmod  33319  opprqusplusg  33460  opprqusmulr  33462  2sqr3nconstr  33771  cos9thpiminplylem1  33772  cos9thpiminplylem5  33776  cos9thpinconstrlem2  33780  lmatfvlem  33805  xrge0iifcnv  33923  lmxrge0  33942  cnrrext  34000  qqtopn  34001  esumrnmpt2  34058  esumpfinvallem  34064  unelldsys  34148  ldgenpisyslem1  34153  measunl  34206  mbfmcst  34250  difelcarsg  34301  carsggect  34309  sibfof  34331  eulerpartlemmf  34366  fib2  34393  fib3  34394  fib4  34395  fib5  34396  fib6  34397  0rrv  34442  coinfliprv  34474  ballotlem2  34480  prodfzo03  34594  chtvalz  34620  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  kur14lem6  35198  kur14lem7  35199  cvmlift2lem12  35301  problem5  35656  quad3  35657  divcnvlin  35720  in-ax8  36212  bj-2upln1upl  37012  bj-rest0  37081  relowlssretop  37351  relowlpssretop  37352  1oequni2o  37356  curunc  37596  ptrest  37613  poimirlem16  37630  poimirlem30  37644  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  itg2addnclem2  37666  ftc1anclem5  37691  ftc1anclem6  37692  sdc  37738  heiborlem3  37807  xrnresex  38392  dmxrncnvepres  38395  dvh4dimN  41441  12gcd5e1  41991  60gcd6e6  41992  60gcd7e1  41993  420gcd8e4  41994  lcmeprodgcdi  41995  lcmineqlem23  42039  sq3deccom12  42278  asin1half  42345  acos1half  42346  redvmptabs  42348  readvrec  42350  sn-it1ei  42425  sn-0tie0  42439  dnnumch1  43033  aomclem6  43048  areaquad  43205  naddov4  43372  unitadd  44184  seff  44298  sblpnf  44299  hashnzfz  44309  lhe4.4ex1a  44318  xrtgcntopre  45474  iccdifioo  45513  itgsin0pilem1  45948  stoweidlem13  46011  stoweidlem26  46024  fourierdlem62  46166  fourierdlem102  46206  fourierdlem114  46218  fourierswlem  46228  fouriersw  46229  sge0tsms  46378  meaiuninc  46479  tworepnotupword  46884  fmtno4prmfac  47570  41prothprm  47617  dfclnbgr4  47822  2zrngasgrp  48231  2zrngmsgrp  48238  tposres3  48866  eloppf  49119  setc1onsubc  49588  mvlraddi  49757  mvlrmuli  49763  i2linesi  49764