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

Theorem eqtr2i 2484
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 2483 . 2  |-  A  =  C
43eqcomi 2467 1  |-  C  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  3eqtrri  2488  3eqtr2ri  2490  dfun3  3699  symdif1  3726  dfif3  3914  dfsn2  4001  prprc1  4096  ssunpr  4146  sstp  4148  unidif0  4576  pwundif  4739  xpindi  5084  xpindir  5085  dmcnvcnv  5173  rncnvcnv  5174  imainrect  5390  dfrn4  5409  fcoi1  5696  foimacnv  5769  fsnunfv  6030  difex2  6496  dfoprab3  6743  offval22  6765  fvmpt2curryd  6903  mapsnconst  7371  sbthlem8  7541  fiint  7702  ordtypecbv  7845  ruv  7930  cantnfOLD  8037  trcl  8062  rankxplim2  8201  infcda1  8476  cfval2  8543  itunitc  8704  ituniiun  8705  hsmex2  8716  ltexnq  9258  ixi  10079  zeo  10841  num0h  10879  dec10p  10898  fseq1p1m1  11654  cats1fvn  12606  fsumrelem  13391  ef0lem  13485  ef01bndlem  13589  sadcadd  13775  sadadd2  13777  mod2xnegi  14221  decexp2  14225  str0  14333  ressinbas  14356  mreexexlem4d  14707  0g0  15556  frmdplusg  15654  oppgplusfval  15985  psgnsn  16148  psgnprfval1  16150  frgpnabllem1  16475  opprmulfval  16843  opprrngb  16850  opprunit  16879  00lsp  17188  psrmulr  17581  ltbwe  17681  ply1plusgfvi  17823  chrval  18084  dsmmelbas  18292  qtopres  19406  ufildr  19639  oppgtmd  19803  tgioo  20508  tgqioo  20512  dveflem  21587  lhop1lem  21621  sincos4thpi  22111  coskpi  22118  cxpsqrlem  22283  log2ublem1  22477  efrlim  22499  basellem3  22556  bposlem9  22767  wlkntrllem2  23631  cnid  24010  ip1ilem  24398  ipasslem10  24411  normlem6  24689  dfhnorm2  24696  h1de2i  25128  spansnji  25221  pjneli  25298  mayetes3i  25305  pjclem1  25771  mdslmd3i  25908  atabsi  25977  imadifxp  26110  xrge00  26312  cnvordtrestixx  26508  raddcn  26524  rrhcn  26591  esumpfinvallem  26688  isrnsigaOLD  26720  sxbrsigalem1  26864  eulerpartgbij  26919  sgnneg  27087  subfacp1lem1  27231  subfacval2  27239  ghomsn  27471  ptrest  28593  mblfinlem3  28598  ismblfin  28600  areacirc  28657  mapfzcons1  29221  lmhmlnmsplit  29608  pwssplit4  29610  wallispilem4  30031  lindslinindsimp2lem5  31148  mat2pmatfval  31232  pmapglb  33772  dvh4dimN  35450  hdmapfval  35833
  Copyright terms: Public domain W3C validator