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

Theorem 3eqtr3ri 2441
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 2434 . 2  |-  B  =  C
51, 4eqtr3i 2434 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  indif2  3552  dfif5  3719  resdm2  5327  co01  5351  funiunfv  5962  dfdom2  7100  1mhlfehlf  10154  crreczi  11467  rei  11924  cos1bnd  12751  rpnnen2lem3  12779  rpnnen2lem11  12787  m1bits  12915  karatsuba  13383  sincos4thpi  20382  sincos6thpi  20384  1cubrlem  20642  cht3  20917  bclbnd  21025  bposlem8  21036  ip1ilem  22288  mdexchi  23799  disjxpin  23989  xppreima  24020  df1stres  24052  df2ndres  24053  ballotth  24756  bpoly3  26016  bpoly4  26017  mbfposadd  26161  stoweidlem26  27650
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2405
  Copyright terms: Public domain W3C validator