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

Theorem eqtr2i 2674
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 2673 . 2 𝐴 = 𝐶
43eqcomi 2660 1 𝐶 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  3eqtrri  2678  3eqtr2ri  2680  dfun3  3898  dfif3  4133  dfsn2  4223  prprc1  4332  diftpsn3  4364  ssunpr  4397  sstp  4399  unidif0  4868  pwundif  5050  xpindi  5288  xpindir  5289  dmcnvcnv  5380  rncnvcnv  5381  imainrect  5610  dfrn4  5630  fcoi1  6116  foimacnv  6192  fsnunfv  6494  difex2  7011  dfoprab3  7268  offval22  7298  fvmpt2curryd  7442  mapsnconst  7945  sbthlem8  8118  fiint  8278  ordtypecbv  8463  ruv  8545  trcl  8642  rankxplim2  8781  infcda1  9053  cfval2  9120  itunitc  9281  ituniiun  9282  hsmex2  9293  ltexnq  9835  ixi  10694  zeo  11501  num0h  11547  dec10p  11591  dec10pOLD  11592  fseq1p1m1  12452  cats1fvn  13649  s3fn  13702  fsumrelem  14583  ef0lem  14853  ef01bndlem  14958  sadcadd  15227  sadadd2  15229  3lcm2e6woprm  15375  mod2xnegi  15822  decexp2  15826  str0  15958  ressinbas  15983  mreexexlem4d  16354  0g0  17310  frmdplusg  17438  sgrp2nmndlem4  17462  sgrp2nmndlem5  17463  oppgplusfval  17824  psgnsn  17986  psgnprfval1  17988  frgpnabllem1  18322  opprmulfval  18671  opprringb  18678  opprunit  18707  00lsp  19029  psrmulr  19432  ltbwe  19520  ply1plusgfvi  19660  chrval  19921  dsmmelbas  20131  mat2pmatfval  20576  unisngl  21378  qtopres  21549  ufildr  21782  oppgtmd  21948  tgioo  22646  tgqioo  22650  dveflem  23787  lhop1lem  23821  sincos4thpi  24310  coskpi  24317  cxpsqrtlem  24493  log2ublem1  24718  efrlim  24741  basellem3  24854  bposlem9  25062  graop  25966  0grsubgr  26215  usgrfilem  26264  finsumvtxdg2ssteplem4  26500  wlkvtxedg  26596  2wlkdlem1  26890  2pthd  26905  wlk2v2e  27135  3wlkdlem1  27137  3pthd  27152  konigsberg  27235  cnidOLD  27565  ip1ilem  27809  ipasslem10  27822  normlem6  28100  dfhnorm2  28107  h1de2i  28540  spansnji  28633  pjneli  28710  mayetes3i  28716  pjclem1  29182  mdslmd3i  29319  atabsi  29388  imadifxp  29540  dfdec100  29704  dpmul100  29733  dpmul1000  29735  dpmul4  29750  xrge00  29814  locfinref  30036  cnvordtrestixx  30087  raddcn  30103  rrhcn  30169  qqtopn  30183  esumpfinvallem  30264  isrnsigaOLD  30303  sxbrsigalem1  30475  eulerpartgbij  30562  sgnneg  30730  hgt750lem2  30858  subfacp1lem1  31287  subfacval2  31295  quad3  31690  ptrest  33538  poimirlem3  33542  poimirlem8  33547  poimirlem15  33554  mblfinlem3  33578  ismblfin  33580  areacirc  33635  pmapglb  35374  dvh4dimN  37053  hdmapfval  37436  mapfzcons1  37597  lmhmlnmsplit  37974  pwssplit4  37976  clcnvlem  38247  cnvrcl0  38249  iunrelexp0  38311  sumnnodd  40180  climinf2mpt  40264  climinfmpt  40265  dvnmul  40476  wallispilem4  40603  dirkertrigeqlem3  40635  fourierdlem24  40666  fourierdlem57  40698  fourierdlem58  40699  fourierdlem80  40721  fourierswlem  40765  fouriersw  40766  fouriercn  40767  subsaliuncl  40894  gsumge0cl  40906  sge0tsms  40915  caragenuncllem  41047  0ome  41064  hoidmvle  41135  ovolval3  41182  ovolval4lem1  41184  smfpimbor1lem2  41327  gbpart7  41980  gbpart9  41982  gbpart11  41983  nnsum3primes4  42001  xpiun  42091  lindslinindsimp2lem5  42576  aacllem  42875
  Copyright terms: Public domain W3C validator