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

Theorem eqtr3i 2675
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 2660 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2673 1 𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  3eqtr3i  2681  3eqtr3ri  2682  unundi  3807  unundir  3808  inindi  3863  inindir  3864  dfin4  3900  difun1  3920  difabs  3925  notab  3930  dif0  3983  difdifdir  4089  tpidm13  4323  intmin2  4536  iunxdif3  4638  univ  4949  iunxpconst  5209  dmres  5454  opabresid  5490  rnresi  5514  cnvcnvOLD  5622  rnresv  5629  cnvsn0  5638  cnvsnOLD  5656  resdmres  5663  coi2  5690  coires1  5691  dfdm2  5705  isarep2  6016  resasplit  6112  ssimaex  6302  fnreseql  6367  resfunexg  6520  idref  6539  mpt2mpt  6794  caov31  6905  fvresex  7181  xpexgALT  7203  1st2val  7238  2nd2val  7239  cnvoprab  7274  fnsuppeq0  7368  ecopovtrn  7893  limensuci  8177  pssnn  8219  r1sucg  8670  jech9.3  8715  rankbnd2  8770  compss  9236  zorn2lem4  9359  iunfo  9399  cardf  9410  alephsuc3  9440  fpwwe2lem13  9502  rankcf  9637  halfnq  9836  addclprlem2  9877  mulgt0sr  9964  mul02lem2  10251  mul02  10252  addid1  10254  mvlladdi  10337  mvllmuli  10896  infrenegsup  11044  8th4div3  11290  nneo  11499  dec10OLD  11593  nummac  11596  numadd  11598  numaddc  11599  nummul1c  11600  9p2e11OLD  11658  decbin0  11720  rpsup  12705  resup  12706  om2uzrdg  12795  m1expcl2  12922  facnn  13102  fac0  13103  faclbnd4lem1  13120  4bc3eq4  13155  hasheq0  13192  f1oun2prg  13708  sqrt1  14056  sqrt4  14057  sqrt9  14058  rddif  14124  abs3lemi  14193  sumss2  14501  divcnvshft  14631  geo2sum2  14649  geomulcvg  14651  geoihalfsum  14658  risefall0lem  14801  bpoly2  14832  bpoly3  14833  sin0  14923  efival  14926  ef01bndlem  14958  cos2bnd  14962  sin4lt0  14969  flodddiv4  15184  2prm  15452  unbenlem  15659  dec5dvds  15815  modxai  15819  mod2xi  15820  mod2xnegi  15822  gcdi  15824  numexp2x  15830  decsplit  15834  decsplitOLD  15838  setsid  15961  mreexexlem3d  16353  oppchom  16422  2oppchomf  16431  isoval  16472  estrres  16826  oppchofcl  16947  oyoncl  16957  mvdco  17911  m1expaddsub  17964  psgn0fv0  17977  oppglsm  18103  dprd2da  18487  ring1  18648  opprsubg  18682  lsppratlem1  19195  opsrtoslem1  19532  ply1basfvi  19659  coe1tm  19691  ply1coe  19714  zzngim  19949  cnmsgnsubg  19971  psgninv  19976  zrhpsgnmhm  19978  neitr  21032  comppfsc  21383  kgeni  21388  xkoinjcn  21538  ufprim  21760  metreslem  22214  restmetu  22422  retopbas  22611  cnfldms  22626  qdensere2  22647  xrsmopn  22662  metdscn2  22707  pcoass  22870  recvs  22992  zclmncvs  22994  iscmet3lem3  23134  cncms  23197  cnfldcusp  23199  resscdrg  23200  rrxprds  23223  ovoliunnul  23321  uniioombllem4  23400  vitalilem5  23426  mbfres  23456  ismbf3d  23466  i1fima  23490  i1fd  23493  itg2cnlem1  23573  itgss3  23626  ellimc2  23686  limccnp2  23701  cpnres  23745  lhop  23824  plyeq0  24012  plypf1  24013  sinhalfpilem  24260  sincos6thpi  24312  sincos3rdpi  24313  pige3  24314  dfrelog  24357  logimul  24405  logneg2  24406  dvlog  24442  cxpsqrt  24494  ang180lem2  24585  ang180lem3  24586  ang180lem4  24587  quart1  24628  asin1  24666  atan0  24680  atanlogsublem  24687  atan1  24700  log2tlbnd  24717  log2ublem2  24719  log2ub  24721  basellem8  24859  cht2  24943  ppiub  24974  bposlem6  25059  bposlem8  25061  bposlem9  25062  lgsdir2lem3  25097  lgseisenlem1  25145  lgseisenlem2  25146  lgsquadlem1  25150  lgsquadlem2  25151  2lgsoddprmlem2  25179  chebbnd1  25206  istrkg3ld  25405  tgcgr4  25471  motplusg  25482  ax5seglem7  25860  ex-un  27411  ex-sqrt  27441  ipdirilem  27812  ipasslem10  27822  hisubcomi  28089  normlem0  28094  norm3difi  28132  norm3lem  28134  polid2i  28142  chdmj1i  28468  chjjdiri  28511  spansn0  28528  pjoml4i  28574  cmbr3i  28587  qlaxr3i  28623  honpcani  28812  honpncani  28814  lnopunilem1  28997  lnophmlem2  29004  lnfn0i  29029  pjbdlni  29136  pjclem1  29182  pjclem3  29184  pjci  29187  atomli  29369  atabs2i  29389  mddmdin0i  29418  difeq  29481  disjdifprg  29514  imadifxp  29540  fnresin  29558  ofpreima2  29594  df1stres  29609  df2ndres  29610  cnvoprabOLD  29626  dfdec100  29704  decdiv10  29732  dpmul100  29733  dpmul1000  29735  dpexpp1  29744  dpadd2  29746  dpadd  29747  dpmul  29749  dpmul4  29750  threehalves  29751  xrge0base  29813  xrge00  29814  xrge0mulgnn0  29817  xrge0slmod  29972  lmatfvlem  30009  xrge0iifcnv  30107  lmxrge0  30126  cnrrext  30182  qqtopn  30183  esumrnmpt2  30258  esumpfinvallem  30264  unelldsys  30349  ldgenpisyslem1  30354  measunl  30407  mbfmcst  30449  difelcarsg  30500  carsggect  30508  sibfof  30530  eulerpartlemmf  30565  fib2  30592  fib3  30593  fib4  30594  fib5  30595  fib6  30596  0rrv  30641  coinfliprv  30672  ballotlem2  30678  prodfzo03  30809  chtvalz  30835  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  kur14lem6  31319  kur14lem7  31320  cvmlift2lem12  31422  problem5  31689  quad3  31690  divcnvlin  31744  logi  31746  bj-2upln1upl  33137  bj-rest0  33171  relowlssretop  33341  relowlpssretop  33342  1oequni2o  33346  curunc  33521  ptrest  33538  poimirlem16  33555  poimirlem30  33569  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  itg2addnclem2  33592  ftc1anclem5  33619  ftc1anclem6  33620  sdc  33670  heiborlem3  33742  xrnresex  34304  dvh4dimN  37053  dnnumch1  37931  aomclem6  37946  areaquad  38119  unitadd  38815  seff  38825  sblpnf  38826  hashnzfz  38836  lhe4.4ex1a  38845  xrtgcntopre  40022  iccdifioo  40059  itgsin0pilem1  40483  stoweidlem13  40548  stoweidlem26  40561  fourierdlem62  40703  fourierdlem102  40743  fourierdlem114  40755  fourierswlem  40765  fouriersw  40766  sge0tsms  40915  meaiuninc  41016  fmtno4prmfac  41809  41prothprm  41861  2zrngasgrp  42265  2zrngmsgrp  42272  mvlraddi  42842  mvlrmuli  42851  i2linesi  42852
  Copyright terms: Public domain W3C validator