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

Theorem eqtr2i 2632
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 2631 . 2 𝐴 = 𝐶
43eqcomi 2618 1 𝐶 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  3eqtrri  2636  3eqtr2ri  2638  dfun3  3823  dfif3  4049  dfsn2  4137  prprc1  4242  diftpsn3  4272  ssunpr  4300  sstp  4302  unidif0  4758  pwundif  4934  xpindi  5164  xpindir  5165  dmcnvcnv  5255  rncnvcnv  5256  imainrect  5479  dfrn4  5498  fcoi1  5975  foimacnv  6051  fsnunfv  6335  difex2  6840  dfoprab3  7092  offval22  7117  fvmpt2curryd  7261  mapsnconst  7766  sbthlem8  7939  fiint  8099  ordtypecbv  8282  ruv  8367  trcl  8464  rankxplim2  8603  infcda1  8875  cfval2  8942  itunitc  9103  ituniiun  9104  hsmex2  9115  ltexnq  9653  ixi  10507  zeo  11297  num0h  11343  dec10p  11387  dec10pOLD  11388  fseq1p1m1  12240  cats1fvn  13402  s3fn  13454  fsumrelem  14328  ef0lem  14596  ef01bndlem  14701  sadcadd  14966  sadadd2  14968  3lcm2e6woprm  15114  mod2xnegi  15561  decexp2  15565  str0  15687  ressinbas  15711  mreexexlem4d  16078  0g0  17034  frmdplusg  17162  sgrp2nmndlem4  17186  sgrp2nmndlem5  17187  oppgplusfval  17549  psgnsn  17711  psgnprfval1  17713  frgpnabllem1  18047  opprmulfval  18396  opprringb  18403  opprunit  18432  00lsp  18750  psrmulr  19153  ltbwe  19241  ply1plusgfvi  19381  chrval  19639  dsmmelbas  19849  mat2pmatfval  20294  unisngl  21087  qtopres  21258  ufildr  21492  oppgtmd  21658  tgioo  22354  tgqioo  22358  dveflem  23490  lhop1lem  23524  sincos4thpi  24013  coskpi  24020  cxpsqrtlem  24192  log2ublem1  24417  efrlim  24440  basellem3  24553  bposlem9  24761  wlkntrllem2  25883  cnidOLD  26614  ip1ilem  26858  ipasslem10  26871  normlem6  27149  dfhnorm2  27156  h1de2i  27589  spansnji  27682  pjneli  27759  mayetes3i  27765  pjclem1  28231  mdslmd3i  28368  atabsi  28437  imadifxp  28589  xrge00  28810  locfinref  29029  cnvordtrestixx  29080  raddcn  29096  rrhcn  29162  qqtopn  29176  esumpfinvallem  29256  isrnsigaOLD  29295  sxbrsigalem1  29467  eulerpartgbij  29554  sgnneg  29722  subfacp1lem1  30208  subfacval2  30216  quad3  30611  ptrest  32361  poimirlem3  32365  poimirlem8  32370  poimirlem15  32377  mblfinlem3  32401  ismblfin  32403  areacirc  32458  pmapglb  33857  dvh4dimN  35537  hdmapfval  35920  mapfzcons1  36081  lmhmlnmsplit  36458  pwssplit4  36460  clcnvlem  36732  cnvrcl0  36734  iunrelexp0  36796  sumnnodd  38480  dvnmul  38616  wallispilem4  38744  dirkertrigeqlem3  38776  fourierdlem24  38807  fourierdlem57  38839  fourierdlem58  38840  fourierdlem80  38862  fourierswlem  38906  fouriersw  38907  fouriercn  38908  subsaliuncl  39035  gsumge0cl  39047  sge0tsms  39056  caragenuncllem  39185  0ome  39202  hoidmvle  39273  ovolval3  39320  ovolval4lem1  39322  smfpimbor1lem2  39467  gbpart7  39973  gbpart9  39975  gbpart11  39976  nnsum3primes4  39988  graop  40243  0grsubgr  40483  usgrfilem  40527  21wlkdlem1  41113  2pthd  41128  1wlk2v2e  41305  31wlkdlem1  41307  3pthd  41322  konigsberg-av  41408  xpiun  41537  lindslinindsimp2lem5  42026  aacllem  42298
  Copyright terms: Public domain W3C validator