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

Theorem eqtr2i 2848
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 2847 . 2 𝐴 = 𝐶
43eqcomi 2833 1 𝐶 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817
This theorem is referenced by:  3eqtrri  2852  3eqtr2ri  2854  dfun3  4227  dfif3  4464  dfsn2  4563  prprc1  4686  diftpsn3  4720  ssunpr  4750  sstp  4752  unidif0  5248  pwundifOLD  5445  xpindi  5692  xpindir  5693  dmcnvcnv  5791  rncnvcnv  5792  imainrect  6026  dfrn4  6047  fcoi1  6541  foimacnv  6621  f1ossf1o  6879  fsnunfv  6938  difex2  7473  dfoprab3  7744  offval22  7775  fvmpocurryd  7929  mapsnconst  8448  sbthlem8  8627  fiint  8788  ordtypecbv  8974  ruv  9059  trcl  9163  rankxplim2  9302  infdju1  9609  cfval2  9676  itunitc  9837  ituniiun  9838  hsmex2  9849  ltexnq  10391  ixi  11263  zeo  12063  num0h  12105  dec10p  12136  fseq1p1m1  12983  cats1fvn  14218  s3fn  14271  fsumrelem  15160  ef0lem  15430  ef01bndlem  15535  sadcadd  15803  sadadd2  15805  3lcm2e6woprm  15955  mod2xnegi  16403  decexp2  16407  str0  16533  ressinbas  16558  mreexexlem4d  16916  0g0  17872  frmdplusg  18017  smndex1bas  18069  sgrp2nmndlem4  18091  sgrp2nmndlem5  18092  oppgplusfval  18474  symgsubmefmnd  18524  psgnsn  18646  psgnprfval1  18648  frgpnabllem1  18991  opprmulfval  19373  opprringb  19380  opprunit  19409  00lsp  19748  ltbwe  20248  ply1plusgfvi  20405  chrval  20667  dsmmelbas  20878  mat2pmatfval  21326  unisngl  22130  qtopres  22301  ufildr  22534  oppgtmd  22700  tgioo  23399  tgqioo  23403  dveflem  24580  lhop1lem  24614  sincos4thpi  25104  coskpi  25113  cxpsqrtlem  25291  log2ublem1  25530  efrlim  25553  basellem3  25666  bposlem9  25874  graop  26820  0grsubgr  27066  usgrfilem  27115  finsumvtxdg2ssteplem4  27336  wlkvtxedg  27431  2wlkdlem1  27709  2pthd  27724  wlk2v2e  27940  3wlkdlem1  27942  3pthd  27957  konigsberg  28040  cnidOLD  28363  ip1ilem  28607  ipasslem10  28620  normlem6  28896  dfhnorm2  28903  h1de2i  29334  spansnji  29427  pjneli  29504  mayetes3i  29510  pjclem1  29976  mdslmd3i  30113  atabsi  30182  imadifxp  30357  dfdec100  30552  dpmul100  30579  dpmul1000  30581  dpmul4  30596  xrge00  30700  cyc2fv1  30790  cyc2fv2  30791  cyc3fv3  30808  locfinref  31135  cnvordtrestixx  31183  raddcn  31199  rrhcn  31265  qqtopn  31279  esumpfinvallem  31360  sxbrsigalem1  31570  eulerpartgbij  31657  sgnneg  31825  hgt750lem2  31950  subfacp1lem1  32453  subfacval2  32461  quad3  32940  ptrest  34968  poimirlem3  34972  poimirlem8  34977  poimirlem15  34984  mblfinlem3  35008  ismblfin  35010  areacirc  35062  pmapglb  36978  dvh4dimN  38655  hdmapfval  39035  12gcd5e1  39199  3lexlogpow5ineq1  39249  sqdeccom12  39357  remul02  39417  mapfzcons1  39514  lmhmlnmsplit  39887  pwssplit4  39889  clcnvlem  40179  cnvrcl0  40181  sqrtcval2  40198  resqrtvalex  40201  imsqrtvalex  40202  iunrelexp0  40259  sumnnodd  42138  climinf2mpt  42222  climinfmpt  42223  dvnmul  42451  wallispilem4  42576  dirkertrigeqlem3  42608  fourierdlem24  42639  fourierdlem57  42671  fourierdlem58  42672  fourierdlem80  42694  fourierswlem  42738  fouriersw  42739  fouriercn  42740  subsaliuncl  42864  gsumge0cl  42876  sge0tsms  42885  caragenuncllem  43017  0ome  43034  hoidmvle  43105  ovolval3  43152  ovolval4lem1  43154  smfpimbor1lem2  43297  gbpart7  44151  gbpart9  44153  gbpart11  44154  nnsum3primes4  44172  xpiun  44252  lindslinindsimp2lem5  44736  ackval42a  44965  aacllem  45183
  Copyright terms: Public domain W3C validator