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

Theorem eqtr2i 2476
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 2475 . 2  |-  A  =  C
43eqcomi 2462 1  |-  C  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-cleq 2446
This theorem is referenced by:  3eqtrri  2480  3eqtr2ri  2482  dfun3  3683  symdif1OLD  3711  dfif3  3897  dfsn2  3983  prprc1  4085  ssunpr  4137  sstp  4139  unidif0  4579  pwundif  4744  xpindi  4971  xpindir  4972  dmcnvcnv  5060  rncnvcnv  5061  imainrect  5281  dfrn4  5299  fcoi1  5762  foimacnv  5836  fsnunfv  6109  difex2  6603  dfoprab3  6854  offval22  6877  fvmpt2curryd  7023  mapsnconst  7522  sbthlem8  7694  fiint  7853  ordtypecbv  8037  ruv  8120  trcl  8217  rankxplim2  8356  infcda1  8628  cfval2  8695  itunitc  8856  ituniiun  8857  hsmex2  8868  ltexnq  9405  ixi  10248  zeo  11028  num0h  11068  dec10p  11087  fseq1p1m1  11875  cats1fvn  12961  s3fn  13009  fsumrelem  13879  ef0lem  14145  ef01bndlem  14250  sadcadd  14444  sadadd2  14446  3lcm2e6woprm  14592  mod2xnegi  15055  decexp2  15059  str0  15173  ressinbas  15197  mreexexlem4d  15565  0g0  16518  frmdplusg  16650  sgrp2nmndlem4  16674  sgrp2nmndlem5  16675  oppgplusfval  17011  psgnsn  17173  psgnprfval1  17175  frgpnabllem1  17521  opprmulfval  17865  opprringb  17872  opprunit  17901  00lsp  18216  psrmulr  18620  ltbwe  18708  ply1plusgfvi  18847  chrval  19108  dsmmelbas  19314  mat2pmatfval  19759  unisngl  20554  qtopres  20725  ufildr  20958  oppgtmd  21124  tgioo  21826  tgqioo  21830  dveflem  22943  lhop1lem  22977  sincos4thpi  23480  coskpi  23487  cxpsqrtlem  23659  log2ublem1  23884  efrlim  23907  basellem3  24021  bposlem9  24232  wlkntrllem2  25302  cnid  26091  ip1ilem  26479  ipasslem10  26492  normlem6  26780  dfhnorm2  26787  h1de2i  27218  spansnji  27311  pjneli  27388  mayetes3i  27394  pjclem1  27860  mdslmd3i  27997  atabsi  28066  imadifxp  28224  xrge00  28460  locfinref  28680  cnvordtrestixx  28731  raddcn  28747  rrhcn  28813  qqtopn  28827  esumpfinvallem  28907  isrnsigaOLD  28946  sxbrsigalem1  29119  eulerpartgbij  29217  sgnneg  29423  subfacp1lem1  29914  subfacval2  29922  quad3  30314  ghomsn  30318  ptrest  31951  poimirlem3  31955  poimirlem8  31960  poimirlem15  31967  mblfinlem3  31991  ismblfin  31993  areacirc  32049  pmapglb  33347  dvh4dimN  35027  hdmapfval  35410  mapfzcons1  35571  lmhmlnmsplit  35957  pwssplit4  35959  clcnvlem  36242  cnvrcl0  36244  iunrelexp0  36306  sumnnodd  37720  dvnmul  37828  wallispilem4  37940  dirkertrigeqlem3  37972  fourierdlem24  38003  fourierdlem57  38037  fourierdlem58  38038  fourierdlem80  38060  fourierswlem  38104  fouriersw  38105  fouriercn  38106  gsumge0cl  38223  sge0tsms  38232  caragenuncllem  38343  0ome  38360  hoidmvle  38432  gbpart7  38878  gbpart9  38880  gbpart11  38881  nnsum3primes4  38893  graop  39141  0grsubgr  39360  usgrfilem  39403  1wlk2v2e  39753  21wlkdlem1  39757  usgfis  39862  xpiun  39870  lindslinindsimp2lem5  40359  aacllem  40644
  Copyright terms: Public domain W3C validator