MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr3i Structured version   Visualization version   GIF version

Theorem eqtr3i 2847
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
StepHypRef Expression
1 eqtr3i.1 . . 3 𝐴 = 𝐵
21eqcomi 2831 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2845 1 𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  3eqtr3i  2853  3eqtr3ri  2854  rabrabi  3468  unundi  4121  unundir  4122  inindi  4177  inindir  4178  dfin4  4218  difun1  4238  difabs  4242  notab  4247  dif0  4304  difdifdir  4409  pwundif  4537  tpidm13  4666  intmin2  4878  iunxdif3  4992  univ  5321  iunxpconst  5601  opabresidOLD  5897  rnresi  5921  rnresv  6036  cnvsn0  6045  resdmres  6067  coi2  6094  coires1  6095  dfdm2  6110  isarep2  6422  resasplit  6529  ssimaex  6730  fnreseql  6800  resfunexg  6960  mpompt  7250  caov31  7362  fvresex  7647  xpexgALT  7668  1st2val  7703  2nd2val  7704  cnvoprab  7744  fnsuppeq0  7845  ecopovtrn  8387  limensuci  8681  pssnn  8724  r1sucg  9186  jech9.3  9231  rankbnd2  9286  djuin  9335  compss  9787  zorn2lem4  9910  iunfo  9950  cardf  9961  alephsuc3  9991  fpwwe2lem13  10053  rankcf  10188  halfnq  10387  addclprlem2  10428  mulgt0sr  10516  mul02lem2  10806  mul02  10807  addid1  10809  mvlladdi  10893  mvllmuli  11462  infrenegsup  11611  8th4div3  11845  nneo  12054  nummac  12131  numadd  12133  numaddc  12134  nummul1c  12135  decbin0  12226  rpsup  13229  resup  13230  om2uzrdg  13319  m1expcl2  13447  facnn  13631  fac0  13632  faclbnd4lem1  13649  4bc3eq4  13684  hasheq0  13720  f1oun2prg  14270  sqrt1  14622  sqrt4  14623  sqrt9  14624  rddif  14691  abs3lemi  14761  sumss2  15074  divcnvshft  15201  geo2sum2  15221  geomulcvg  15223  geoihalfsum  15229  risefall0lem  15371  bpoly2  15402  bpoly3  15403  sin0  15493  efival  15496  ef01bndlem  15528  cos2bnd  15532  sin4lt0  15539  flodddiv4  15753  2prm  16025  unbenlem  16233  dec5dvds  16389  modxai  16393  mod2xi  16394  mod2xnegi  16396  gcdi  16398  numexp2x  16404  decsplit  16408  setsid  16529  mreexexlem3d  16908  oppchom  16976  2oppchomf  16985  isoval  17026  estrres  17380  oppchofcl  17501  oyoncl  17511  mvdco  18564  m1expaddsub  18617  psgn0fv0  18630  oppglsm  18758  dprd2da  19155  ring1  19346  opprsubg  19380  lsppratlem1  19910  zzngim  20242  cnmsgnsubg  20264  psgninv  20269  zrhpsgnmhm  20271  ply1basfvi  20868  coe1tm  20900  ply1coe  20923  neitr  21783  comppfsc  22135  kgeni  22140  xkoinjcn  22290  ufprim  22512  metreslem  22967  restmetu  23175  retopbas  23364  cnfldms  23379  qdensere2  23400  xrsmopn  23415  metdscn2  23460  pcoass  23627  recvs  23749  zclmncvs  23751  iscmet3lem3  23892  cncms  23957  cnfldcusp  23959  resscdrg  23960  rrxprds  23991  ovoliunnul  24109  uniioombllem4  24188  vitalilem5  24214  mbfres  24246  ismbf3d  24256  i1fima  24280  i1fd  24283  itg2cnlem1  24363  itgss3  24416  ellimc2  24478  limccnp2  24493  cpnres  24538  lhop  24617  plyeq0  24806  plypf1  24807  sinhalfpilem  25054  sincos6thpi  25106  sincos3rdpi  25107  pige3ALT  25110  dfrelog  25155  logimul  25203  logneg2  25204  dvlog  25240  cxpsqrt  25292  ang180lem2  25394  ang180lem3  25395  ang180lem4  25396  quart1  25440  asin1  25478  atan0  25492  atanlogsublem  25499  atan1  25512  log2tlbnd  25529  log2ublem2  25531  log2ub  25533  basellem8  25671  cht2  25755  ppiub  25786  bposlem6  25871  bposlem8  25873  bposlem9  25874  lgsdir2lem3  25909  lgseisenlem1  25957  lgseisenlem2  25958  lgsquadlem1  25962  lgsquadlem2  25963  2lgsoddprmlem2  25991  chebbnd1  26054  istrkg3ld  26253  tgcgr4  26323  motplusg  26334  ax5seglem7  26727  ex-un  28207  ex-sqrt  28237  ipdirilem  28610  ipasslem10  28620  hisubcomi  28885  normlem0  28890  norm3difi  28928  norm3lem  28930  polid2i  28938  chdmj1i  29262  chjjdiri  29305  spansn0  29322  pjoml4i  29368  cmbr3i  29381  qlaxr3i  29417  honpcani  29606  honpncani  29608  lnopunilem1  29791  lnophmlem2  29798  lnfn0i  29823  pjbdlni  29930  pjclem1  29976  pjclem3  29978  pjci  29981  atomli  30163  atabs2i  30183  mddmdin0i  30212  disjdifr  30281  difeq  30287  disjdifprg  30333  imadifxp  30359  fnresin  30379  ofpreima2  30419  df1stres  30447  df2ndres  30448  cnvoprabOLD  30466  dfdec100  30556  decdiv10  30582  dpmul100  30583  dpmul1000  30585  dpexpp1  30594  dpadd2  30596  dpadd  30597  dpmul  30599  dpmul4  30600  threehalves  30601  xrge0base  30703  xrge00  30704  xrge0mulgnn0  30707  tocycfvres1  30783  tocycfvres2  30784  cycpmfvlem  30785  cycpmfv3  30788  cycpmcl  30789  cyc2fv1  30794  cyc3conja  30830  xrge0slmod  30949  lmatfvlem  31137  xrge0iifcnv  31250  lmxrge0  31269  cnrrext  31325  qqtopn  31326  esumrnmpt2  31401  esumpfinvallem  31407  unelldsys  31491  ldgenpisyslem1  31496  measunl  31549  mbfmcst  31591  difelcarsg  31642  carsggect  31650  sibfof  31672  eulerpartlemmf  31707  fib2  31734  fib3  31735  fib4  31736  fib5  31737  fib6  31738  0rrv  31783  coinfliprv  31814  ballotlem2  31820  prodfzo03  31948  chtvalz  31974  hgt750lemd  31993  hgt750lem  31996  hgt750lem2  31997  kur14lem6  32532  kur14lem7  32533  cvmlift2lem12  32635  problem5  32986  quad3  32987  divcnvlin  33038  logi  33040  bj-2upln1upl  34421  bj-rest0  34469  relowlssretop  34741  relowlpssretop  34742  1oequni2o  34746  curunc  34998  ptrest  35015  poimirlem16  35032  poimirlem30  35046  mblfinlem2  35054  ovoliunnfl  35058  voliunnfl  35060  itg2addnclem2  35068  ftc1anclem5  35093  ftc1anclem6  35094  sdc  35141  heiborlem3  35210  xrnresex  35773  dvh4dimN  38702  12gcd5e1  39253  60gcd6e6  39254  60gcd7e1  39255  420gcd8e4  39256  lcmeprodgcdi  39257  lcmineqlem23  39301  3lexlogpow5ineq1  39303  sq3deccom12  39429  imulid1  39517  sn-inelr  39525  dnnumch1  39919  aomclem6  39934  areaquad  40097  unitadd  40835  seff  40948  sblpnf  40949  hashnzfz  40959  lhe4.4ex1a  40968  xrtgcntopre  42058  iccdifioo  42092  itgsin0pilem1  42532  stoweidlem13  42595  stoweidlem26  42608  fourierdlem62  42750  fourierdlem102  42790  fourierdlem114  42802  fourierswlem  42812  fouriersw  42813  sge0tsms  42959  meaiuninc  43060  fmtno4prmfac  44029  41prothprm  44077  2zrngasgrp  44504  2zrngmsgrp  44511  mvlraddi  45238  mvlrmuli  45245  i2linesi  45246
  Copyright terms: Public domain W3C validator