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

Theorem 3eqtr3ri 2467
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 2460 . 2  |-  B  =  C
51, 4eqtr3i 2460 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  indif2  3722  dfif5  3931  resdm2  5345  co01  5370  funiunfv  6168  dfdom2  7602  1mhlfehlf  10832  crreczi  12394  rei  13198  bpoly3  14089  bpoly4  14090  cos1bnd  14219  rpnnen2lem3  14247  rpnnen2lem11  14255  m1bits  14388  6gcd4e2  14476  3lcm2e6  14652  karatsuba  15019  ring1  17765  sincos4thpi  23333  sincos6thpi  23335  1cubrlem  23632  cht3  23963  bclbnd  24071  bposlem8  24082  ex-ind-dvds  25744  ip1ilem  26312  mdexchi  27823  disjxpin  28037  xppreima  28088  df1stres  28124  df2ndres  28125  xrge0slmod  28446  cnrrext  28653  ballotth  29196  poimirlem3  31647  poimirlem30  31674  mbfposadd  31692  asindmre  31731  areaquad  35800  inductionexd  36230  stoweidlem26  37455  3exp4mod41  38306
  Copyright terms: Public domain W3C validator