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

Theorem eqtr2i 2432
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 2431 . 2  |-  A  =  C
43eqcomi 2415 1  |-  C  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394
This theorem is referenced by:  3eqtrri  2436  3eqtr2ri  2438  dfun3  3687  symdif1OLD  3715  dfif3  3898  dfsn2  3984  prprc1  4081  ssunpr  4133  sstp  4135  unidif0  4566  pwundif  4729  xpindi  4956  xpindir  4957  dmcnvcnv  5045  rncnvcnv  5046  imainrect  5265  dfrn4  5283  fcoi1  5741  foimacnv  5815  fsnunfv  6090  difex2  6588  dfoprab3  6839  offval22  6862  fvmpt2curryd  7002  mapsnconst  7501  sbthlem8  7671  fiint  7830  ordtypecbv  7975  ruv  8059  cantnfOLD  8165  trcl  8190  rankxplim2  8329  infcda1  8604  cfval2  8671  itunitc  8832  ituniiun  8833  hsmex2  8844  ltexnq  9382  ixi  10218  zeo  10988  num0h  11028  dec10p  11047  fseq1p1m1  11805  cats1fvn  12877  fsumrelem  13770  ef0lem  14021  ef01bndlem  14126  sadcadd  14315  sadadd2  14317  mod2xnegi  14764  decexp2  14768  str0  14879  ressinbas  14902  mreexexlem4d  15259  0g0  16212  frmdplusg  16344  sgrp2nmndlem4  16368  sgrp2nmndlem5  16369  oppgplusfval  16705  psgnsn  16867  psgnprfval1  16869  frgpnabllem1  17199  opprmulfval  17592  opprringb  17599  opprunit  17628  00lsp  17945  psrmulr  18355  ltbwe  18455  ply1plusgfvi  18601  chrval  18860  dsmmelbas  19066  mat2pmatfval  19514  unisngl  20318  qtopres  20489  ufildr  20722  oppgtmd  20886  tgioo  21591  tgqioo  21595  dveflem  22670  lhop1lem  22704  sincos4thpi  23196  coskpi  23203  cxpsqrtlem  23375  log2ublem1  23600  efrlim  23623  basellem3  23735  bposlem9  23946  wlkntrllem2  24966  cnid  25753  ip1ilem  26141  ipasslem10  26154  normlem6  26432  dfhnorm2  26439  h1de2i  26871  spansnji  26964  pjneli  27041  mayetes3i  27047  pjclem1  27513  mdslmd3i  27650  atabsi  27719  imadifxp  27880  xrge00  28112  locfinref  28283  cnvordtrestixx  28334  raddcn  28350  rrhcn  28416  esumpfinvallem  28507  isrnsigaOLD  28546  sxbrsigalem1  28719  eulerpartgbij  28803  sgnneg  28971  subfacp1lem1  29463  subfacval2  29471  quad3  29863  ghomsn  29867  ptrest  31400  mblfinlem3  31405  ismblfin  31407  areacirc  31463  pmapglb  32767  dvh4dimN  34447  hdmapfval  34830  mapfzcons1  34991  lmhmlnmsplit  35375  pwssplit4  35377  iunrelexp0  35661  sumnnodd  36985  dvnmul  37089  wallispilem4  37199  dirkertrigeqlem3  37231  fourierdlem24  37262  fourierdlem57  37295  fourierdlem58  37296  fourierdlem80  37318  fourierswlem  37362  fouriersw  37363  fouriercn  37364  gbpart7  37802  gbpart9  37804  gbpart11  37805  nnsum3primes4  37817  usgfis  38056  xpiun  38064  lindslinindsimp2lem5  38555  aacllem  38841
  Copyright terms: Public domain W3C validator