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

Theorem eqtr3i 2488
Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)
Hypotheses
Ref Expression
eqtr3i.1  |-  A  =  B
eqtr3i.2  |-  A  =  C
Assertion
Ref Expression
eqtr3i  |-  B  =  C

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3  |-  A  =  B
21eqcomi 2470 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2486 1  |-  B  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
This theorem is referenced by:  3eqtr3i  2494  3eqtr3ri  2495  unundi  3661  unundir  3662  inindi  3711  inindir  3712  dfin4  3745  difun1  3765  difabs  3769  notab  3775  dif0  3901  difdifdir  3918  tpidm13  4134  tpprceq3  4172  intmin2  4316  univ  4707  iunxpconst  5065  dmres  5304  opabresid  5337  rnresi  5360  cnvcnv  5465  rnresv  5472  cnvsn0  5482  cnvsn  5497  resdmres  5504  coi2  5530  coires1  5531  dfdm2  5545  isarep2  5674  resasplit  5761  ssimaex  5938  fnreseql  5998  fnsuppeq0OLD  6133  resfunexg  6138  idref  6154  mpt2mpt  6393  caov31  6503  fvresex  6772  xpexgALT  6792  1st2val  6825  2nd2val  6826  fnsuppeq0  6946  ecopovtrn  7432  limensuci  7712  pssnn  7757  r1sucg  8204  jech9.3  8249  rankbnd2  8304  compss  8773  zorn2lem4  8896  iunfo  8931  cardf  8942  alephsuc3  8972  fpwwe2lem13  9037  rankcf  9172  halfnq  9371  addclprlem2  9412  mulgt0sr  9499  mul02lem2  9774  mul02  9775  addid1  9777  mvlladdi  9856  mvllmuli  10398  infmsup  10541  8th4div3  10780  nneo  10967  dec10  11030  nummac  11032  numadd  11034  numaddc  11035  nummul1c  11036  9p2e11  11062  decbin0  11103  rpsup  11996  resup  11997  om2uzrdg  12070  m1expcl2  12191  binom2aiOLD  12281  facnn  12358  fac0  12359  faclbnd4lem1  12374  hasheq0  12436  f1oun2prg  12877  sqrt1  13117  sqrt4  13118  sqrt9  13119  rddif  13185  abs3lemi  13254  sumss2  13560  geo2sum2  13695  geomulcvg  13697  geoihalfsum  13703  sin0  13896  efival  13899  ef01bndlem  13931  cos2bnd  13935  sin4lt0  13942  2prm  14245  unbenlem  14438  dec5dvds  14562  modxai  14566  mod2xi  14567  mod2xnegi  14569  gcdi  14571  numexp2x  14577  decsplit  14581  setsid  14687  mreexexlem3d  15063  oppchom  15131  2oppchomf  15140  isoval  15181  estrres  15535  oppchofcl  15656  oyoncl  15666  mvdco  16597  m1expaddsub  16650  psgn0fv0  16663  oppglsm  16789  dprd2da  17218  ring1  17375  opprsubg  17412  lsppratlem1  17920  opsrtoslem1  18275  ply1basfvi  18409  coe1tm  18441  ply1coe  18464  ply1coeOLD  18465  zzngim  18718  cnmsgnsubg  18740  psgninv  18745  zrhpsgnmhm  18747  neitr  19808  comppfsc  20159  kgeni  20164  xkoinjcn  20314  ufprim  20536  metreslem  20991  restmetu  21216  retopbas  21393  cnfldms  21409  qdensere2  21428  xrsmopn  21443  metdscn2  21487  pcoass  21650  iscmet3lem3  21855  cncms  21921  cnfldcusp  21923  resscdrg  21924  rrxprds  21947  ovoliunnul  22044  uniioombllem4  22121  vitalilem5  22147  mbfres  22177  ismbf3d  22187  i1fima  22211  i1fd  22214  itg2cnlem1  22294  itgss3  22347  ellimc2  22407  limccnp2  22422  cpnres  22466  lhop  22543  plyeq0  22734  plypf1  22735  sinhalfpilem  22982  sincos6thpi  23034  sincos3rdpi  23035  pige3  23036  dfrelog  23079  logimul  23125  logneg2  23126  dvlog  23158  cxpsqrt  23210  ang180lem2  23268  ang180lem3  23269  ang180lem4  23270  quart1  23313  asin1  23351  atan0  23365  atanlogsublem  23372  atan1  23385  log2tlbnd  23402  log2ublem2  23404  log2ub  23406  basellem8  23487  cht2  23572  ppiub  23605  bposlem6  23690  bposlem8  23692  bposlem9  23693  lgsdir2lem3  23726  lgseisenlem1  23750  lgseisenlem2  23751  lgsquadlem1  23755  lgsquadlem2  23756  chebbnd1  23783  motplusg  24055  ax5seglem7  24365  ex-un  25272  circgrpOLD  25503  ipdirilem  25871  ipasslem10  25881  hisubcomi  26148  normlem0  26153  norm3difi  26191  norm3lem  26193  polid2i  26201  chdmj1i  26526  chjjdiri  26569  spansn0  26586  pjoml4i  26632  cmbr3i  26645  qlaxr3i  26681  honpcani  26871  honpncani  26873  lnopunilem1  27056  lnophmlem2  27063  lnfn0i  27088  pjbdlni  27195  pjclem1  27241  pjclem3  27243  pjci  27246  atomli  27428  atabs2i  27448  mddmdin0i  27477  difeq  27544  iunxdif3  27566  disjdifprg  27575  imadifxp  27600  fnresin  27617  ofpreima2  27662  df1stres  27677  df2ndres  27678  cnvoprab  27703  xrge0base  27833  xrge00  27834  xrge0mulgnn0  27837  xrge0slmod  27995  ordtconlem1  28067  xrge0iifcnv  28076  lmxrge0  28095  cnrrext  28152  esumrnmpt2  28240  esumpfinvallem  28246  measvuni  28358  measunl  28360  measinb  28365  mbfmcst  28403  difelcarsg  28453  sibfof  28479  eulerpartlemmf  28511  fib2  28538  fib3  28539  fib4  28540  fib5  28541  fib6  28542  0rrv  28587  coinfliprv  28618  ballotlem2  28624  ballotlemgun  28660  kur14lem6  28852  kur14lem7  28853  cvmlift2lem12  28956  problem5  29220  quad3  29221  4bc3eq4  29329  divcnvshft  29335  divcnvlin  29336  logi  29339  risefall0lem  29366  bpoly2  30024  bpoly3  30025  ptrest  30253  mblfinlem2  30257  ovoliunnfl  30261  voliunnfl  30263  itg2addnclem2  30272  ftc1anclem5  30299  ftc1anclem6  30300  sdc  30442  heiborlem3  30514  dnnumch1  31194  aomclem6  31209  areaquad  31388  seff  31393  sblpnf  31394  hashnzfz  31429  lhe4.4ex1a  31438  iccdifioo  31758  itgsin0pilem1  31951  stoweidlem13  31998  stoweidlem26  32011  fourierdlem62  32154  fourierdlem102  32194  fourierdlem114  32206  fourierswlem  32216  fouriersw  32217  2zrngasgrp  32890  2zrngmsgrp  32897  mvlraddi  33324  mvlrmuli  33336  i2linesi  33337  bj-2upln1upl  34725  dvh4dimN  37317  unitadd  38208
  Copyright terms: Public domain W3C validator