Theorem eqtr3i 2788

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

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  3eqtr3i  2794  3eqtr3ri  2795  unundi  4129  unundir  4130  inindi  4187  inindir  4188  dfin4  4231  difun1  4252  difabs  4256  notab  4267  dif0  4334  difdifdir  4452  pwundif  4587  tpidm13  4722  intmin2  4940  iunxdif3  5061  univ  5432  iunxpconst  5734  resdmdfsn  6031  rnresi  6077  rnresv  6200  imadifssran  6202  cnvsn0  6211  resdmres  6233  coi2  6265  coires1  6266  dfdm2  6282  isarep2  6625  resasplit  6748  ssimaex  6966  fnreseql  7043  resfunexg  7213  mpompt  7524  caov31  7639  fvresex  7953  xpexgALT  7974  1st2val  8010  2nd2val  8011  cnvoprab  8053  fnsuppeq0  8184  ecopovtrn  8814  limensuci  9137  pwfilem  9273  r1sucg  9737  jech9.3  9782  rankbnd2  9837  djuin  9900  compss  10355  zorn2lem4  10478  iunfo  10518  cardf  10529  alephsuc3  10560  fpwwe2lem12  10622  rankcf  10757  halfnq  10956  addclprlem2  10997  mulgt0sr  11085  mul02lem2  11382  mul02  11383  addrid  11385  mvlladdi  11471  mvllmuli  12043  infrenegsup  12193  halfpm6th  12461  nneo  12675  nummac  12756  numadd  12758  numaddc  12759  nummul1c  12760  decbin0  12853  fz00m1  13569  rpsup  13895  resup  13896  om2uzrdg  13988  m1expcl2  14117  facnn  14307  fac0  14308  faclbnd4lem1  14325  4bc3eq4  14360  hasheq0  14395  f1oun2prg  14950  sqrt1  15318  sqrt4  15319  sqrt9  15320  rddif  15388  abs3lemi  15458  sumss2  15773  divcnvshft  15905  geo2sum2  15924  geomulcvg  15926  geoihalfsum  15932  bpoly2  16106  bpoly3  16107  sin0  16200  efival  16203  ef01bndlem  16235  cos2bnd  16239  sin4lt0  16246  flodddiv4  16468  2prm  16745  unbenlem  16963  dec5dvds  17119  modxai  17123  mod2xi  17124  mod2xnegi  17126  gcdi  17128  numexp2x  17133  decsplit  17137  setsid  17262  xrge0base  17656  mreexexlem3d  17697  oppchom  17766  2oppchomf  17775  isoval  17817  estrres  18190  oppchofcl  18311  oyoncl  18321  mvdco  19510  m1expaddsub  19563  psgn0fv0  19576  oppglsm  19707  dprd2da  20109  ring1  20389  opprsubg  20430  lsppratlem1  21271  pzriprnglem7  21637  zzngim  21702  cnmsgnsubg  21727  psgninv  21732  zrhpsgnmhm  21734  ply1basfvi  22400  coe1tm  22434  ply1coe  22458  comppfsc  23689  kgeni  23694  xkoinjcn  23844  ufprim  24066  metreslem  24519  retopbas  24917  cnfldms  24932  qdensere2  24954  xrsmopn  24970  metdscn2  25015  pcoass  25183  recvs  25305  zclmncvs  25307  iscmet3lem3  25449  cncms  25514  cnfldcusp  25516  resscdrg  25517  rrxprds  25548  ovoliunnul  25666  uniioombllem4  25745  vitalilem5  25771  mbfres  25803  ismbf3d  25813  i1fima  25837  i1fd  25840  itg2cnlem1  25920  itgss3  25974  ellimc2  26036  limccnp2  26051  cpnres  26096  lhop  26175  plyeq0  26368  plypf1  26369  sinhalfpilem  26628  sincos6thpi  26681  sincos3rdpi  26682  pige3ALT  26685  dfrelog  26730  logi  26752  logimul  26779  logneg2  26780  dvlog  26816  cxpsqrt  26868  ang180lem2  26975  ang180lem3  26976  ang180lem4  26977  quart1  27021  asin1  27059  atan0  27073  atanlogsublem  27080  atan1  27093  log2tlbnd  27110  log2ublem2  27112  log2ub  27114  cht2  27336  ppiub  27368  bposlem6  27453  bposlem8  27455  bposlem9  27456  lgsdir2lem3  27491  lgseisenlem1  27539  lgseisenlem2  27540  lgsquadlem1  27544  lgsquadlem2  27545  2lgsoddprmlem2  27573  chebbnd1  27636  negbdaylem  28249  om2noseqrdg  28497  zseo  28615  bdaypw2n0bndlem  28656  istrkg3ld  28730  tgcgr4  28800  motplusg  28811  ax5seglem7  29285  ex-un  30775  ex-sqrt  30805  ipdirilem  31181  ipasslem10  31191  hisubcomi  31456  normlem0  31461  norm3difi  31499  norm3lem  31501  polid2i  31509  chdmj1i  31833  chjjdiri  31876  spansn0  31893  pjoml4i  31939  cmbr3i  31952  qlaxr3i  31988  honpcani  32177  honpncani  32179  lnopunilem1  32362  lnophmlem2  32369  lnfn0i  32394  pjbdlni  32501  pjclem1  32547  pjclem3  32549  pjci  32552  atomli  32734  atabs2i  32754  mddmdin0i  32783  imadifxp  32946  fnresin  32969  ofpreima2  33011  df1stres  33049  df2ndres  33050  nn0disj01  33163  dfdec100  33174  decdiv10  33215  dpmul100  33216  dpmul1000  33218  dpexpp1  33227  dpadd2  33229  dpadd  33230  dpmul  33232  dpmul4  33233  threehalves  33234  xrge00  33334  xrge0mulgnn0  33335  cyc2fv1  33441  cyc3conja  33477  elrgspnlem4  33565  xrge0slmod  33668  opprqusplusg  33771  opprqusmulr  33773  selvply1rhmlemb  33909  extvfvcl  33926  2sqr3nconstr  34171  cos9thpiminplylem1  34172  cos9thpiminplylem5  34176  cos9thpinconstrlem2  34180  lmatfvlem  34205  xrge0iifcnv  34323  lmxrge0  34342  cnrrext  34400  qqtopn  34401  esumrnmpt2  34458  esumpfinvallem  34464  unelldsys  34548  ldgenpisyslem1  34553  measunl  34606  mbfmcst  34649  difelcarsg  34700  carsggect  34708  sibfof  34730  eulerpartlemmf  34765  fib2  34792  fib3  34793  fib4  34794  fib5  34795  fib6  34796  0rrv  34841  coinfliprv  34873  ballotlem2  34879  prodfzo03  34990  chtvalz  35016  hgt750lemd  35035  hgt750lem  35038  hgt750lem2  35039  1enumen  35485  kur14lem6  35703  kur14lem7  35704  cvmlift2lem12  35806  problem5  36161  quad3  36162  divcnvlin  36225  in-ax8  36736  bj-2upln1upl  37660  bj-rest0  37735  relowlssretop  38009  relowlpssretop  38010  1oequni2o  38014  curunc  38253  ptrest  38270  poimirlem16  38287  poimirlem30  38301  mblfinlem2  38309  ovoliunnfl  38313  voliunnfl  38315  itg2addnclem2  38323  ftc1anclem5  38348  ftc1anclem6  38349  sdc  38395  heiborlem3  38464  xrnresex  39078  dmxrncnvepres  39081  dvh4dimN  42221  12gcd5e1  42770  60gcd6e6  42771  60gcd7e1  42772  420gcd8e4  42773  lcmeprodgcdi  42774  lcmineqlem23  42818  25or6to4  42973  sq3deccom12  43051  asin1half  43118  acos1half  43119  redvmptabs  43121  readvrec  43123  sn-it1ei  43198  sn-0tie0  43225  dnnumch1  43771  aomclem6  43786  areaquad  43943  naddov4  44110  unitadd  44921  seff  45019  sblpnf  45020  hashnzfz  45030  lhe4.4ex1a  45039  xrtgcntopre  46192  iccdifioo  46231  itgsin0pilem1  46664  stoweidlem13  46727  stoweidlem26  46740  fourierdlem62  46882  fourierdlem102  46922  fourierdlem114  46934  fourierswlem  46944  fouriersw  46945  sge0tsms  47094  meaiuninc  47195  cos5t  47616  fmtno4prmfac  48324  41prothprm  48371  ppivalnn4  48379  dfclnbgr4  48589  2zrngasgrp  49011  2zrngmsgrp  49018  tposres3  49659  eloppf  49911  setc1onsubc  50380  mvlraddi  50549  mvlrmuli  50555  i2linesi  50556