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

Theorem 3eqtr3ri 2459
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 2452 . 2  |-  B  =  C
51, 4eqtr3i 2452 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  indif2  3571  dfif5  3738  resdm2  5346  co01  5370  funiunfv  5981  dfdom2  7119  1mhlfehlf  10174  crreczi  11487  rei  11944  cos1bnd  12771  rpnnen2lem3  12799  rpnnen2lem11  12807  m1bits  12935  karatsuba  13403  sincos4thpi  20404  sincos6thpi  20406  1cubrlem  20664  cht3  20939  bclbnd  21047  bposlem8  21058  ip1ilem  22310  mdexchi  23821  disjxpin  24011  xppreima  24042  df1stres  24074  df2ndres  24075  ballotth  24778  bpoly3  26047  bpoly4  26048  mbfposadd  26195  stoweidlem26  27684
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2423
  Copyright terms: Public domain W3C validator