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

Theorem eqtr2i 2473
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 2472 . 2  |-  A  =  C
43eqcomi 2456 1  |-  C  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  3eqtrri  2477  3eqtr2ri  2479  dfun3  3721  symdif1  3748  dfif3  3940  dfsn2  4027  prprc1  4125  ssunpr  4177  sstp  4179  unidif0  4610  pwundif  4777  xpindi  5126  xpindir  5127  dmcnvcnv  5215  rncnvcnv  5216  imainrect  5438  dfrn4  5457  fcoi1  5749  foimacnv  5823  fsnunfv  6096  difex2  6592  dfoprab3  6841  offval22  6864  fvmpt2curryd  7002  mapsnconst  7466  sbthlem8  7636  fiint  7799  ordtypecbv  7945  ruv  8030  cantnfOLD  8137  trcl  8162  rankxplim2  8301  infcda1  8576  cfval2  8643  itunitc  8804  ituniiun  8805  hsmex2  8816  ltexnq  9356  ixi  10185  zeo  10955  num0h  10996  dec10p  11015  fseq1p1m1  11763  cats1fvn  12805  fsumrelem  13603  ef0lem  13796  ef01bndlem  13901  sadcadd  14090  sadadd2  14092  mod2xnegi  14539  decexp2  14543  str0  14652  ressinbas  14675  mreexexlem4d  15026  0g0  15869  frmdplusg  16001  sgrp2nmndlem4  16025  sgrp2nmndlem5  16026  oppgplusfval  16362  psgnsn  16524  psgnprfval1  16526  frgpnabllem1  16856  opprmulfval  17253  opprringb  17260  opprunit  17289  00lsp  17606  psrmulr  18016  ltbwe  18116  ply1plusgfvi  18262  chrval  18540  dsmmelbas  18748  mat2pmatfval  19202  unisngl  20006  qtopres  20177  ufildr  20410  oppgtmd  20574  tgioo  21279  tgqioo  21283  dveflem  22358  lhop1lem  22392  sincos4thpi  22884  coskpi  22891  cxpsqrtlem  23061  log2ublem1  23255  efrlim  23277  basellem3  23334  bposlem9  23545  wlkntrllem2  24540  cnid  25331  ip1ilem  25719  ipasslem10  25732  normlem6  26010  dfhnorm2  26017  h1de2i  26449  spansnji  26542  pjneli  26619  mayetes3i  26626  pjclem1  27092  mdslmd3i  27229  atabsi  27298  imadifxp  27436  xrge00  27652  locfinref  27822  cnvordtrestixx  27873  raddcn  27889  rrhcn  27956  esumpfinvallem  28058  isrnsigaOLD  28090  sxbrsigalem1  28234  eulerpartgbij  28289  sgnneg  28457  subfacp1lem1  28601  subfacval2  28609  quad3  29002  ghomsn  29006  ptrest  30024  mblfinlem3  30029  ismblfin  30031  areacirc  30088  mapfzcons1  30625  lmhmlnmsplit  31009  pwssplit4  31011  sumnnodd  31590  dvnmul  31694  wallispilem4  31804  dirkertrigeqlem3  31836  fourierdlem24  31867  fourierdlem57  31900  fourierdlem58  31901  fourierdlem80  31923  fourierswlem  31967  fouriersw  31968  fouriercn  31969  usgfis  32400  xpiun  32408  lindslinindsimp2lem5  32933  pmapglb  35369  dvh4dimN  37049  hdmapfval  37432
  Copyright terms: Public domain W3C validator