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

Theorem eqtr2i 2452
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 2451 . 2  |-  A  =  C
43eqcomi 2435 1  |-  C  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-cleq 2414
This theorem is referenced by:  3eqtrri  2456  3eqtr2ri  2458  dfun3  3711  symdif1OLD  3739  dfif3  3923  dfsn2  4009  prprc1  4107  ssunpr  4159  sstp  4161  unidif0  4594  pwundif  4757  xpindi  4984  xpindir  4985  dmcnvcnv  5073  rncnvcnv  5074  imainrect  5294  dfrn4  5312  fcoi1  5771  foimacnv  5845  fsnunfv  6116  difex2  6609  dfoprab3  6860  offval22  6883  fvmpt2curryd  7023  mapsnconst  7522  sbthlem8  7692  fiint  7851  ordtypecbv  8035  ruv  8118  trcl  8214  rankxplim2  8353  infcda1  8624  cfval2  8691  itunitc  8852  ituniiun  8853  hsmex2  8864  ltexnq  9401  ixi  10242  zeo  11022  num0h  11062  dec10p  11081  fseq1p1m1  11869  cats1fvn  12945  fsumrelem  13855  ef0lem  14121  ef01bndlem  14226  sadcadd  14420  sadadd2  14422  3lcm2e6woprm  14568  mod2xnegi  15031  decexp2  15035  str0  15149  ressinbas  15173  mreexexlem4d  15541  0g0  16494  frmdplusg  16626  sgrp2nmndlem4  16650  sgrp2nmndlem5  16651  oppgplusfval  16987  psgnsn  17149  psgnprfval1  17151  frgpnabllem1  17497  opprmulfval  17841  opprringb  17848  opprunit  17877  00lsp  18192  psrmulr  18596  ltbwe  18684  ply1plusgfvi  18823  chrval  19083  dsmmelbas  19289  mat2pmatfval  19734  unisngl  20529  qtopres  20700  ufildr  20933  oppgtmd  21099  tgioo  21801  tgqioo  21805  dveflem  22918  lhop1lem  22952  sincos4thpi  23455  coskpi  23462  cxpsqrtlem  23634  log2ublem1  23859  efrlim  23882  basellem3  23996  bposlem9  24207  wlkntrllem2  25276  cnid  26065  ip1ilem  26453  ipasslem10  26466  normlem6  26754  dfhnorm2  26761  h1de2i  27192  spansnji  27285  pjneli  27362  mayetes3i  27368  pjclem1  27834  mdslmd3i  27971  atabsi  28040  imadifxp  28202  xrge00  28443  locfinref  28664  cnvordtrestixx  28715  raddcn  28731  rrhcn  28797  qqtopn  28811  esumpfinvallem  28891  isrnsigaOLD  28930  sxbrsigalem1  29103  eulerpartgbij  29201  sgnneg  29407  subfacp1lem1  29898  subfacval2  29906  quad3  30298  ghomsn  30302  ptrest  31853  poimirlem3  31857  poimirlem8  31862  poimirlem15  31869  mblfinlem3  31893  ismblfin  31895  areacirc  31951  pmapglb  33254  dvh4dimN  34934  hdmapfval  35317  mapfzcons1  35478  lmhmlnmsplit  35865  pwssplit4  35867  iunrelexp0  36154  sumnnodd  37530  dvnmul  37638  wallispilem4  37750  dirkertrigeqlem3  37782  fourierdlem24  37813  fourierdlem57  37847  fourierdlem58  37848  fourierdlem80  37870  fourierswlem  37914  fouriersw  37915  fouriercn  37916  gsumge0cl  38001  sge0tsms  38010  caragenuncllem  38112  0ome  38129  gbpart7  38580  gbpart9  38582  gbpart11  38583  nnsum3primes4  38595  graop  38794  usgfis  39030  xpiun  39038  lindslinindsimp2lem5  39529  aacllem  39814
  Copyright terms: Public domain W3C validator