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

Theorem eqtr2i 2633
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1 𝐴 = 𝐵
eqtr2i.2 𝐵 = 𝐶
Assertion
Ref Expression
eqtr2i 𝐶 = 𝐴

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3 𝐴 = 𝐵
2 eqtr2i.2 . . 3 𝐵 = 𝐶
31, 2eqtri 2632 . 2 𝐴 = 𝐶
43eqcomi 2619 1 𝐶 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-cleq 2603
This theorem is referenced by:  3eqtrri  2637  3eqtr2ri  2639  dfun3  3824  dfif3  4050  dfsn2  4138  prprc1  4243  diftpsn3  4273  ssunpr  4305  sstp  4307  unidif0  4764  pwundif  4945  xpindi  5177  xpindir  5178  dmcnvcnv  5269  rncnvcnv  5270  imainrect  5494  dfrn4  5513  fcoi1  5991  foimacnv  6067  fsnunfv  6358  difex2  6863  dfoprab3  7115  offval22  7140  fvmpt2curryd  7284  mapsnconst  7789  sbthlem8  7962  fiint  8122  ordtypecbv  8305  ruv  8390  trcl  8487  rankxplim2  8626  infcda1  8898  cfval2  8965  itunitc  9126  ituniiun  9127  hsmex2  9138  ltexnq  9676  ixi  10535  zeo  11339  num0h  11385  dec10p  11429  dec10pOLD  11430  fseq1p1m1  12283  cats1fvn  13454  s3fn  13506  fsumrelem  14380  ef0lem  14648  ef01bndlem  14753  sadcadd  15018  sadadd2  15020  3lcm2e6woprm  15166  mod2xnegi  15613  decexp2  15617  str0  15739  ressinbas  15763  mreexexlem4d  16130  0g0  17086  frmdplusg  17214  sgrp2nmndlem4  17238  sgrp2nmndlem5  17239  oppgplusfval  17601  psgnsn  17763  psgnprfval1  17765  frgpnabllem1  18099  opprmulfval  18448  opprringb  18455  opprunit  18484  00lsp  18802  psrmulr  19205  ltbwe  19293  ply1plusgfvi  19433  chrval  19692  dsmmelbas  19902  mat2pmatfval  20347  unisngl  21140  qtopres  21311  ufildr  21545  oppgtmd  21711  tgioo  22407  tgqioo  22411  dveflem  23546  lhop1lem  23580  sincos4thpi  24069  coskpi  24076  cxpsqrtlem  24248  log2ublem1  24473  efrlim  24496  basellem3  24609  bposlem9  24817  graop  25706  wlkntrllem2  26090  cnidOLD  26821  ip1ilem  27065  ipasslem10  27078  normlem6  27356  dfhnorm2  27363  h1de2i  27796  spansnji  27889  pjneli  27966  mayetes3i  27972  pjclem1  28438  mdslmd3i  28575  atabsi  28644  imadifxp  28796  xrge00  29017  locfinref  29236  cnvordtrestixx  29287  raddcn  29303  rrhcn  29369  qqtopn  29383  esumpfinvallem  29463  isrnsigaOLD  29502  sxbrsigalem1  29674  eulerpartgbij  29761  sgnneg  29929  subfacp1lem1  30415  subfacval2  30423  quad3  30818  ptrest  32578  poimirlem3  32582  poimirlem8  32587  poimirlem15  32594  mblfinlem3  32618  ismblfin  32620  areacirc  32675  pmapglb  34074  dvh4dimN  35754  hdmapfval  36137  mapfzcons1  36298  lmhmlnmsplit  36675  pwssplit4  36677  clcnvlem  36949  cnvrcl0  36951  iunrelexp0  37013  sumnnodd  38697  dvnmul  38833  wallispilem4  38961  dirkertrigeqlem3  38993  fourierdlem24  39024  fourierdlem57  39056  fourierdlem58  39057  fourierdlem80  39079  fourierswlem  39123  fouriersw  39124  fouriercn  39125  subsaliuncl  39252  gsumge0cl  39264  sge0tsms  39273  caragenuncllem  39402  0ome  39419  hoidmvle  39490  ovolval3  39537  ovolval4lem1  39539  smfpimbor1lem2  39684  gbpart7  40189  gbpart9  40191  gbpart11  40192  nnsum3primes4  40204  0grsubgr  40502  usgrfilem  40546  21wlkdlem1  41132  2pthd  41147  1wlk2v2e  41324  31wlkdlem1  41326  3pthd  41341  konigsberg-av  41427  xpiun  41556  lindslinindsimp2lem5  42045  aacllem  42356
  Copyright terms: Public domain W3C validator