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

Theorem eqtr2i 2765
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 2764 . 2 𝐴 = 𝐶
43eqcomi 2745 1 𝐶 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728
This theorem is referenced by:  3eqtrri  2769  3eqtr2ri  2771  dfun3  4205  dfif3  4479  dfsn2  4578  prprc1  4705  diftpsn3  4741  ssunpr  4771  sstp  4773  unidif0  5291  xpindi  5755  xpindir  5756  dmcnvcnv  5854  rncnvcnv  5855  imainrect  6099  dfrn4  6120  predres  6257  fcoi1  6678  foimacnv  6763  f1ossf1o  7032  fsnunfv  7091  difex2  7642  dfoprab3  7926  offval22  7960  fvmpocurryd  8118  mapsnconst  8711  sbthlem8  8915  fiint  9139  ordtypecbv  9324  trcl  9534  rankxplim2  9686  infdju1  9995  cfval2  10066  itunitc  10227  ituniiun  10228  hsmex2  10239  ltexnq  10781  ixi  11654  zeo  12456  num0h  12499  dec10p  12530  fseq1p1m1  13380  cats1fvn  14620  s3fn  14673  fsumrelem  15568  ef0lem  15837  ef01bndlem  15942  sadcadd  16214  sadadd2  16216  3lcm2e6woprm  16369  mod2xnegi  16821  decexp2  16825  str0  16939  ressinbas  17004  mreexexlem4d  17405  0g0  18397  frmdplusg  18542  smndex1bas  18594  sgrp2nmndlem4  18616  sgrp2nmndlem5  18617  oppgplusfval  19001  symgsubmefmnd  19055  psgnsn  19177  psgnprfval1  19179  frgpnabllem1  19523  opprmulfval  19913  opprringb  19923  opprunit  19952  00lsp  20292  chrval  20778  dsmmelbas  20995  ltbwe  21294  ply1plusgfvi  21462  mat2pmatfval  21921  unisngl  22727  qtopres  22898  ufildr  23131  oppgtmd  23297  tgioo  24008  tgqioo  24012  dveflem  25192  lhop1lem  25226  sincos4thpi  25719  coskpi  25728  cxpsqrtlem  25906  log2ublem1  26145  efrlim  26168  basellem3  26281  bposlem9  26489  graop  27448  0grsubgr  27694  usgrfilem  27743  finsumvtxdg2ssteplem4  27964  wlkvtxedg  28060  2wlkdlem1  28339  2pthd  28354  wlk2v2e  28570  3wlkdlem1  28572  3pthd  28587  konigsberg  28670  cnidOLD  28993  ip1ilem  29237  ipasslem10  29250  normlem6  29526  dfhnorm2  29533  h1de2i  29964  spansnji  30057  pjneli  30134  mayetes3i  30140  pjclem1  30606  mdslmd3i  30743  atabsi  30812  imadifxp  30989  dfdec100  31193  dpmul100  31220  dpmul1000  31222  dpmul4  31237  xrge00  31344  cyc2fv1  31437  cyc2fv2  31438  cyc3fv3  31455  locfinref  31840  cnvordtrestixx  31912  raddcn  31928  rrhcn  31996  qqtopn  32010  esumpfinvallem  32091  sxbrsigalem1  32301  eulerpartgbij  32388  sgnneg  32556  hgt750lem2  32681  subfacp1lem1  33190  subfacval2  33198  quad3  33677  madeun  34115  ptrest  35824  poimirlem3  35828  poimirlem8  35833  poimirlem15  35840  mblfinlem3  35864  ismblfin  35866  areacirc  35918  pmapglb  37984  dvh4dimN  39661  hdmapfval  40041  12gcd5e1  40211  sqdeccom12  40512  remul02  40583  mapfzcons1  40734  lmhmlnmsplit  41108  pwssplit4  41110  clcnvlem  41444  cnvrcl0  41446  sqrtcval2  41463  resqrtvalex  41466  imsqrtvalex  41467  iunrelexp0  41523  sumnnodd  43400  climinf2mpt  43484  climinfmpt  43485  dvnmul  43713  wallispilem4  43838  dirkertrigeqlem3  43870  fourierdlem24  43901  fourierdlem57  43933  fourierdlem58  43934  fourierdlem80  43956  fourierswlem  44000  fouriersw  44001  fouriercn  44002  subsaliuncl  44126  gsumge0cl  44139  sge0tsms  44148  caragenuncllem  44280  0ome  44297  hoidmvle  44368  ovolval3  44415  ovolval4lem1  44417  smfpimbor1lem2  44567  gbpart7  45463  gbpart9  45465  gbpart11  45466  nnsum3primes4  45484  xpiun  45564  lindslinindsimp2lem5  46047  ackval42a  46287  aacllem  46749
  Copyright terms: Public domain W3C validator