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 setvar class
Syntax hints:    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431
This theorem is referenced by:  3eqtrri  2463  3eqtr2ri  2465  dfun3  3583  symdif1  3610  dfif3  3798  dfsn2  3885  prprc1  3980  ssunpr  4030  sstp  4032  unidif0  4460  pwundif  4623  xpindi  4968  xpindir  4969  dmcnvcnv  5057  rncnvcnv  5058  imainrect  5274  dfrn4  5293  fcoi1  5580  foimacnv  5653  fsnunfv  5913  difex2  6378  dfoprab3  6625  offval22  6647  mapsnconst  7250  sbthlem8  7420  fiint  7580  ordtypecbv  7723  ruv  7808  cantnfOLD  7915  trcl  7940  rankxplim2  8079  infcda1  8354  cfval2  8421  itunitc  8582  ituniiun  8583  hsmex2  8594  ltexnq  9136  ixi  9957  zeo  10719  num0h  10757  dec10p  10776  fseq1p1m1  11526  cats1fvn  12477  fsumrelem  13262  ef0lem  13356  ef01bndlem  13460  sadcadd  13646  sadadd2  13648  mod2xnegi  14092  decexp2  14096  str0  14204  ressinbas  14226  mreexexlem4d  14577  0g0  15426  frmdplusg  15523  oppgplusfval  15854  psgnprfval1  16017  frgpnabllem1  16342  opprmulfval  16705  opprrngb  16712  opprunit  16741  00lsp  17039  psrmulr  17432  ltbwe  17529  ply1plusgfvi  17672  chrval  17931  dsmmelbas  18139  qtopres  19246  ufildr  19479  oppgtmd  19643  tgioo  20348  tgqioo  20352  dveflem  21426  lhop1lem  21460  sincos4thpi  21950  coskpi  21957  cxpsqrlem  22122  log2ublem1  22316  efrlim  22338  basellem3  22395  bposlem9  22606  wlkntrllem2  23410  cnid  23789  ip1ilem  24177  ipasslem10  24190  normlem6  24468  dfhnorm2  24475  h1de2i  24907  spansnji  25000  pjneli  25077  mayetes3i  25084  pjclem1  25550  mdslmd3i  25687  atabsi  25756  imadifxp  25890  xrge00  26098  cnvordtrestixx  26295  raddcn  26311  rrhcn  26378  esumpfinvallem  26475  isrnsigaOLD  26507  sxbrsigalem1  26652  eulerpartgbij  26707  sgnneg  26875  subfacp1lem1  27019  subfacval2  27027  ghomsn  27258  ptrest  28378  mblfinlem3  28383  ismblfin  28385  areacirc  28442  mapfzcons1  29006  lmhmlnmsplit  29393  pwssplit4  29395  wallispilem4  29816  psgnsn  30722  lindslinindsimp2lem5  30885  pmapglb  33254  dvh4dimN  34932  hdmapfval  35315
  Copyright terms: Public domain W3C validator