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

Theorem eqtr2i 2494
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1  |-  A  =  B
eqtr2i.2  |-  B  =  C
Assertion
Ref Expression
eqtr2i  |-  C  =  A

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3  |-  A  =  B
2 eqtr2i.2 . . 3  |-  B  =  C
31, 2eqtri 2493 . 2  |-  A  =  C
43eqcomi 2480 1  |-  C  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-cleq 2464
This theorem is referenced by:  3eqtrri  2498  3eqtr2ri  2500  dfun3  3672  symdif1OLD  3700  dfif3  3886  dfsn2  3972  prprc1  4073  ssunpr  4126  sstp  4128  unidif0  4574  pwundif  4746  xpindi  4973  xpindir  4974  dmcnvcnv  5063  rncnvcnv  5064  imainrect  5284  dfrn4  5303  fcoi1  5769  foimacnv  5845  fsnunfv  6120  difex2  6617  dfoprab3  6868  offval22  6891  fvmpt2curryd  7036  mapsnconst  7535  sbthlem8  7707  fiint  7866  ordtypecbv  8050  ruv  8133  trcl  8230  rankxplim2  8369  infcda1  8641  cfval2  8708  itunitc  8869  ituniiun  8870  hsmex2  8881  ltexnq  9418  ixi  10263  zeo  11044  num0h  11084  dec10p  11103  fseq1p1m1  11894  cats1fvn  13013  s3fn  13065  fsumrelem  13944  ef0lem  14210  ef01bndlem  14315  sadcadd  14511  sadadd2  14513  3lcm2e6woprm  14659  mod2xnegi  15122  decexp2  15126  str0  15239  ressinbas  15263  mreexexlem4d  15631  0g0  16584  frmdplusg  16716  sgrp2nmndlem4  16740  sgrp2nmndlem5  16741  oppgplusfval  17077  psgnsn  17239  psgnprfval1  17241  frgpnabllem1  17587  opprmulfval  17931  opprringb  17938  opprunit  17967  00lsp  18282  psrmulr  18685  ltbwe  18773  ply1plusgfvi  18912  chrval  19173  dsmmelbas  19379  mat2pmatfval  19824  unisngl  20619  qtopres  20790  ufildr  21024  oppgtmd  21190  tgioo  21892  tgqioo  21896  dveflem  23010  lhop1lem  23044  sincos4thpi  23547  coskpi  23554  cxpsqrtlem  23726  log2ublem1  23951  efrlim  23974  basellem3  24088  bposlem9  24299  wlkntrllem2  25369  cnid  26160  ip1ilem  26548  ipasslem10  26561  normlem6  26849  dfhnorm2  26856  h1de2i  27287  spansnji  27380  pjneli  27457  mayetes3i  27463  pjclem1  27929  mdslmd3i  28066  atabsi  28135  imadifxp  28288  xrge00  28523  locfinref  28742  cnvordtrestixx  28793  raddcn  28809  rrhcn  28875  qqtopn  28889  esumpfinvallem  28969  isrnsigaOLD  29008  sxbrsigalem1  29180  eulerpartgbij  29278  sgnneg  29484  subfacp1lem1  29974  subfacval2  29982  quad3  30374  ghomsn  30378  ptrest  32003  poimirlem3  32007  poimirlem8  32012  poimirlem15  32019  mblfinlem3  32043  ismblfin  32045  areacirc  32101  pmapglb  33406  dvh4dimN  35086  hdmapfval  35469  mapfzcons1  35630  lmhmlnmsplit  36016  pwssplit4  36018  clcnvlem  36301  cnvrcl0  36303  iunrelexp0  36365  sumnnodd  37807  dvnmul  37915  wallispilem4  38042  dirkertrigeqlem3  38074  fourierdlem24  38105  fourierdlem57  38139  fourierdlem58  38140  fourierdlem80  38162  fourierswlem  38206  fouriersw  38207  fouriercn  38208  gsumge0cl  38327  sge0tsms  38336  caragenuncllem  38452  0ome  38469  hoidmvle  38540  ovolval3  38587  ovolval4lem1  38589  gbpart7  39013  gbpart9  39015  gbpart11  39016  nnsum3primes4  39028  graop  39284  0grsubgr  39514  usgrfilem  39557  1wlk2v2e  40045  21wlkdlem1  40047  2pthd  40062  31wlkdlem1  40073  3pthd  40088  konigsberg-av  40171  usgfis  40266  xpiun  40274  lindslinindsimp2lem5  40763  aacllem  41046
  Copyright terms: Public domain W3C validator