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

Theorem 3eqtr3ri 2387
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 2380 . 2  |-  B  =  C
51, 4eqtr3i 2380 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1642
This theorem is referenced by:  indif2  3488  dfif5  3653  resdm2  5245  co01  5269  funiunfv  5861  dfdom2  6975  1mhlfehlf  10026  crreczi  11319  rei  11737  cos1bnd  12564  rpnnen2lem3  12592  rpnnen2lem11  12600  m1bits  12728  karatsuba  13196  sincos4thpi  19988  sincos6thpi  19990  1cubrlem  20248  cht3  20523  bclbnd  20631  bposlem8  20642  ip1ilem  21518  mdexchi  23029  df1stres  23295  df2ndres  23296  coinflippvt  23991  ballotth  24044  bpoly3  25352  bpoly4  25353  stoweidlem26  27098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2351
  Copyright terms: Public domain W3C validator