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

Theorem 3eqtr3ri 2495
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 2488 . 2  |-  B  =  C
51, 4eqtr3i 2488 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
This theorem is referenced by:  indif2  3748  dfif5  3960  resdm2  5503  co01  5528  funiunfv  6161  dfdom2  7560  1mhlfehlf  10779  crreczi  12293  rei  13000  cos1bnd  13933  rpnnen2lem3  13961  rpnnen2lem11  13969  m1bits  14101  karatsuba  14581  ring1  17374  sincos4thpi  23031  sincos6thpi  23033  1cubrlem  23297  cht3  23572  bclbnd  23680  bposlem8  23691  ex-ind-dvds  25296  ip1ilem  25867  mdexchi  27380  disjxpin  27584  xppreima  27630  df1stres  27670  df2ndres  27671  xrge0slmod  27987  cnrrext  28144  ballotth  28651  bpoly3  29982  bpoly4  29983  mbfposadd  30224  asindmre  30264  areaquad  31346  3lcm2e6  31381  stoweidlem26  31969  inductionexd  38068
  Copyright terms: Public domain W3C validator