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

Theorem 3eqtr4ri 2494
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 2486 . 2
4 3eqtr4i.2 . 2
53, 4eqtr4i 2486 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1370
This theorem is referenced by:  cbvreucsf  3435  dfin3  3703  dfif6  3908  qdass  4091  tpidm12  4093  unipr  4221  iinvdif  4359  unidif0  4582  csbcnv  5140  dfdm4  5149  dmun  5163  resres  5240  inres  5245  resiun1  5246  imainrect  5398  coundi  5458  coundir  5459  funopg  5569  csbov  6254  elrnmpt2res  6337  offres  6705  1st2val  6735  2nd2val  6736  mpt2mptsx  6770  oeoalem  7169  omopthlem1  7228  snec  7297  tcsni  8100  infmap2  8524  ackbij2lem3  8547  itunisuc  8725  axmulass  9461  divmul13i  10229  dfnn3  10474  halfpm6th  10684  numsucc  10920  decbin2  10998  uzrdgxfr  11934  hashxplem  12353  ids1  12447  fsumadd  13373  fsum2d  13396  bezout  13884  ressbas  14387  oppchomf  14818  oppr1  16902  opsrtoslem1  17742  m2detleiblem2  18702  cnfldnm  20757  volres  21410  voliunlem1  21431  uniioombllem4  21466  itg11  21569  plyid  22077  coeidp  22130  dgrid  22131  dfrelog  22417  log2ublem3  22743  bposlem8  23030  ginvsn  24305  ip2i  24697  bcseqi  24991  hilnormi  25034  cmcmlem  25463  fh3i  25495  fh4i  25496  pjadjii  25546  cnvoprab  26490  resf1o  26497  ressplusf  26572  resvsca  26755  xpinpreima  26793  cnre2csqima  26798  eulerpartgbij  27211  ballotth  27376  plymulx  27405  fprodmul  27927  elrn3  28029  domep  28062  bpoly3  28657  itg2addnclem2  28904  areaquad  30052  stoweidlem13  30542  wallispi2  30602  fourierdlem113  30749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
  Copyright terms: Public domain W3C validator