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

Theorem 3eqtr3ri 2313
Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
Hypotheses
Ref Expression
3eqtr3i.1  |-  A  =  B
3eqtr3i.2  |-  A  =  C
3eqtr3i.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3ri  |-  D  =  C

Proof of Theorem 3eqtr3ri
StepHypRef Expression
1 3eqtr3i.3 . 2  |-  B  =  D
2 3eqtr3i.1 . . 3  |-  A  =  B
3 3eqtr3i.2 . . 3  |-  A  =  C
42, 3eqtr3i 2306 . 2  |-  B  =  C
51, 4eqtr3i 2306 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  indif2  3413  dfif5  3578  resdm2  5161  co01  5185  funiunfv  5736  dfdom2  6883  1mhlfehlf  9930  crreczi  11222  rei  11637  cos1bnd  12463  rpnnen2lem3  12491  rpnnen2lem11  12499  m1bits  12627  karatsuba  13095  sincos4thpi  19877  sincos6thpi  19879  1cubrlem  20133  cht3  20407  bclbnd  20515  bposlem8  20526  ip1ilem  21398  mdexchi  22911  ballotth  23092  bpoly3  24203  bpoly4  24204  cntrset  25013  stoweidlem26  27186
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-cleq 2277
  Copyright terms: Public domain W3C validator