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

Theorem eqtr2i 2459
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 2458 . 2  |-  A  =  C
43eqcomi 2442 1  |-  C  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1653
This theorem is referenced by:  3eqtrri  2463  3eqtr2ri  2465  dfun3  3581  symdif1  3608  dfif3  3751  dfsn2  3830  prprc1  3916  ssunpr  3963  sstp  3965  unidif0  4375  pwundif  4493  difex2  4717  xpindi  5011  xpindir  5012  dmcnvcnv  5095  rncnvcnv  5096  imainrect  5315  dfrn4  5334  fcoi1  5620  foimacnv  5695  fsnunfv  5936  dfoprab3  6406  mapsnconst  7062  sbthlem8  7227  fiint  7386  ordtypecbv  7489  ruv  7571  cantnf  7652  trcl  7667  rankxplim2  7809  infcda1  8078  cfval2  8145  itunitc  8306  ituniiun  8307  hsmex2  8318  ltexnq  8857  ixi  9656  zeo  10360  num0h  10397  dec10p  10416  fseq1p1m1  11127  cats1fvn  11827  fsumrelem  12591  ef0lem  12686  ef01bndlem  12790  sadcadd  12975  sadadd2  12977  mod2xnegi  13412  decexp2  13416  str0  13510  ressinbas  13530  mreexexlem4d  13877  0g0  14714  frmdplusg  14804  oppgplusfval  15149  frgpnabllem1  15489  opprmulfval  15735  opprrngb  15742  opprunit  15771  00lsp  16062  psrmulr  16453  ltbwe  16538  ply1plusgfvi  16641  chrval  16811  qtopres  17735  ufildr  17968  oppgtmd  18132  tgioo  18832  tgqioo  18836  dveflem  19868  lhop1lem  19902  sincos4thpi  20426  coskpi  20433  cxpsqrlem  20598  log2ublem1  20791  efrlim  20813  basellem3  20870  bposlem9  21081  wlkntrllem2  21565  cnid  21944  ip1ilem  22332  ipasslem10  22345  normlem6  22622  dfhnorm2  22629  h1de2i  23060  spansnji  23153  pjneli  23230  mayetes3i  23237  pjclem1  23703  mdslmd3i  23840  atabsi  23909  imadifxp  24043  xrge00  24213  cnvordtrestixx  24316  raddcn  24320  esumpfinvallem  24469  isrnsigaOLD  24500  sxbrsigalem1  24640  subfacp1lem1  24870  subfacval2  24878  ghomsn  25104  mblfinlem3  26257  ismblfin  26259  areacirc  26311  mapfzcons1  26787  lmhmlnmsplit  27176  pwssplit4  27182  dsmmelbas  27196  wallispilem4  27807  pmapglb  30641  dvh4dimN  32319  hdmapfval  32702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator