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

Theorem eqtr2i 2425
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 2424 . 2  |-  A  =  C
43eqcomi 2408 1  |-  C  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  3eqtrri  2429  3eqtr2ri  2431  dfun3  3539  symdif1  3566  dfif3  3709  dfsn2  3788  prprc1  3874  ssunpr  3921  sstp  3923  unidif0  4332  pwundif  4450  difex2  4673  xpindi  4967  xpindir  4968  dmcnvcnv  5051  rncnvcnv  5052  imainrect  5271  dfrn4  5290  fcoi1  5576  foimacnv  5651  fsnunfv  5892  dfoprab3  6362  mapsnconst  7018  sbthlem8  7183  fiint  7342  ordtypecbv  7442  ruv  7524  cantnf  7605  trcl  7620  rankxplim2  7760  infcda1  8029  cfval2  8096  itunitc  8257  ituniiun  8258  hsmex2  8269  ltexnq  8808  ixi  9607  zeo  10311  num0h  10348  dec10p  10367  fseq1p1m1  11077  cats1fvn  11777  fsumrelem  12541  ef0lem  12636  ef01bndlem  12740  sadcadd  12925  sadadd2  12927  mod2xnegi  13362  decexp2  13366  str0  13460  ressinbas  13480  mreexexlem4d  13827  0g0  14664  frmdplusg  14754  oppgplusfval  15099  frgpnabllem1  15439  opprmulfval  15685  opprrngb  15692  opprunit  15721  00lsp  16012  psrmulr  16403  ltbwe  16488  ply1plusgfvi  16591  chrval  16761  qtopres  17683  ufildr  17916  oppgtmd  18080  tgioo  18780  tgqioo  18784  dveflem  19816  lhop1lem  19850  sincos4thpi  20374  coskpi  20381  cxpsqrlem  20546  log2ublem1  20739  efrlim  20761  basellem3  20818  bposlem9  21029  wlkntrllem2  21513  cnid  21892  ip1ilem  22280  ipasslem10  22293  normlem6  22570  dfhnorm2  22577  h1de2i  23008  spansnji  23101  pjneli  23178  mayetes3i  23185  pjclem1  23651  mdslmd3i  23788  atabsi  23857  imadifxp  23991  xrge00  24161  cnvordtrestixx  24264  raddcn  24268  esumpfinvallem  24417  isrnsigaOLD  24448  sxbrsigalem1  24588  subfacp1lem1  24818  subfacval2  24826  ghomsn  25052  mblfinlem2  26144  ismblfin  26146  areacirc  26187  mapfzcons1  26663  lmhmlnmsplit  27053  pwssplit4  27059  dsmmelbas  27073  wallispilem4  27684  pmapglb  30252  dvh4dimN  31930  hdmapfval  32313
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator