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

Theorem eqtr2i 2497
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1  |-  A  =  B
eqtr2i.2  |-  B  =  C
Assertion
Ref Expression
eqtr2i  |-  C  =  A

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3  |-  A  =  B
2 eqtr2i.2 . . 3  |-  B  =  C
31, 2eqtri 2496 . 2  |-  A  =  C
43eqcomi 2480 1  |-  C  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  3eqtrri  2501  3eqtr2ri  2503  dfun3  3736  symdif1  3763  dfif3  3953  dfsn2  4040  prprc1  4137  ssunpr  4189  sstp  4191  unidif0  4620  pwundif  4787  xpindi  5135  xpindir  5136  dmcnvcnv  5224  rncnvcnv  5225  imainrect  5447  dfrn4  5466  fcoi1  5758  foimacnv  5832  fsnunfv  6100  difex2  6586  dfoprab3  6840  offval22  6862  fvmpt2curryd  7000  mapsnconst  7464  sbthlem8  7634  fiint  7796  ordtypecbv  7941  ruv  8026  cantnfOLD  8133  trcl  8158  rankxplim2  8297  infcda1  8572  cfval2  8639  itunitc  8800  ituniiun  8801  hsmex2  8812  ltexnq  9352  ixi  10177  zeo  10945  num0h  10985  dec10p  11004  fseq1p1m1  11751  cats1fvn  12785  fsumrelem  13583  ef0lem  13675  ef01bndlem  13779  sadcadd  13966  sadadd2  13968  mod2xnegi  14415  decexp2  14419  str0  14527  ressinbas  14550  mreexexlem4d  14901  0g0  15750  frmdplusg  15851  oppgplusfval  16185  psgnsn  16348  psgnprfval1  16350  frgpnabllem1  16677  opprmulfval  17070  opprrngb  17077  opprunit  17106  00lsp  17422  psrmulr  17824  ltbwe  17924  ply1plusgfvi  18070  chrval  18345  dsmmelbas  18553  mat2pmatfval  19007  qtopres  19950  ufildr  20183  oppgtmd  20347  tgioo  21052  tgqioo  21056  dveflem  22131  lhop1lem  22165  sincos4thpi  22655  coskpi  22662  cxpsqrtlem  22827  log2ublem1  23021  efrlim  23043  basellem3  23100  bposlem9  23311  wlkntrllem2  24254  cnid  25045  ip1ilem  25433  ipasslem10  25446  normlem6  25724  dfhnorm2  25731  h1de2i  26163  spansnji  26256  pjneli  26333  mayetes3i  26340  pjclem1  26806  mdslmd3i  26943  atabsi  27012  imadifxp  27147  xrge00  27352  cnvordtrestixx  27547  raddcn  27563  rrhcn  27630  esumpfinvallem  27736  isrnsigaOLD  27768  sxbrsigalem1  27912  eulerpartgbij  27967  sgnneg  28135  subfacp1lem1  28279  subfacval2  28287  ghomsn  28519  ptrest  29641  mblfinlem3  29646  ismblfin  29648  areacirc  29705  mapfzcons1  30269  lmhmlnmsplit  30653  pwssplit4  30655  sumnnodd  31188  wallispilem4  31384  fourierdlem24  31447  fourierdlem73  31496  fourierdlem80  31503  fourierdlem81  31504  fourierdlem102  31525  fourierdlem114  31537  fouriercnp  31543  fourierswlem  31547  fouriersw  31548  usgfis  31929  lindslinindsimp2lem5  32153  pmapglb  34575  dvh4dimN  36253  hdmapfval  36636
  Copyright terms: Public domain W3C validator