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

Theorem 3eqtr3ri 2500
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 2493 . 2  |-  B  =  C
51, 4eqtr3i 2493 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-cleq 2454
This theorem is referenced by:  indif2  3736  dfif5  3950  resdm2  5490  co01  5515  funiunfv  6141  dfdom2  7533  1mhlfehlf  10749  crreczi  12248  rei  12941  cos1bnd  13774  rpnnen2lem3  13802  rpnnen2lem11  13810  m1bits  13940  karatsuba  14420  sincos4thpi  22634  sincos6thpi  22636  1cubrlem  22895  cht3  23170  bclbnd  23278  bposlem8  23289  ip1ilem  25405  mdexchi  26918  disjxpin  27108  xppreima  27147  df1stres  27182  df2ndres  27183  xrge0slmod  27485  ballotth  28104  bpoly3  29385  bpoly4  29386  mbfposadd  29628  asindmre  29668  areaquad  30780  stoweidlem26  31283
  Copyright terms: Public domain W3C validator