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

Theorem 3eqtr4ri 2497
Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1
3eqtr4i.2
3eqtr4i.3
Assertion
Ref Expression
3eqtr4ri

Proof of Theorem 3eqtr4ri
StepHypRef Expression
1 3eqtr4i.3 . . 3
2 3eqtr4i.1 . . 3
31, 2eqtr4i 2489 . 2
4 3eqtr4i.2 . 2
53, 4eqtr4i 2489 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395
This theorem is referenced by:  cbvreucsf  3468  dfin3  3736  dfif6  3944  qdass  4129  tpidm12  4131  unipr  4262  iinvdif  4402  unidif0  4625  csbcnv  5191  dfdm4  5200  dmun  5214  resres  5291  inres  5296  resiun1  5297  imainrect  5453  coundi  5513  coundir  5514  funopg  5625  csbov  6331  elrnmpt2res  6416  offres  6795  1st2val  6826  2nd2val  6827  mpt2mptsx  6863  oeoalem  7264  omopthlem1  7323  snec  7393  tcsni  8195  infmap2  8619  ackbij2lem3  8642  itunisuc  8820  axmulass  9555  divmul13i  10330  dfnn3  10575  halfpm6th  10785  numsucc  11030  decbin2  11108  uzrdgxfr  12077  hashxplem  12491  ids1  12609  fsumadd  13561  fsum2d  13586  fprodmul  13765  bezout  14180  ressbas  14687  oppchomf  15115  oppr1  17283  opsrtoslem1  18148  m2detleiblem2  19130  cnfldnm  21286  volres  21939  voliunlem1  21960  uniioombllem4  21995  itg11  22098  plyid  22606  coeidp  22660  dgrid  22661  dfrelog  22953  log2ublem3  23279  bposlem8  23566  ginvsn  25351  ip2i  25743  bcseqi  26037  hilnormi  26080  cmcmlem  26509  fh3i  26541  fh4i  26542  pjadjii  26592  cnvoprab  27546  resf1o  27553  ressplusf  27638  resvsca  27820  xpinpreima  27888  cnre2csqima  27893  eulerpartgbij  28311  ballotth  28476  plymulx  28505  elrn3  29192  domep  29225  bpoly3  29820  itg2addnclem2  30067  areaquad  31184  stoweidlem13  31795  wallispi2  31855  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem113  32002  fourierswlem  32013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator