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

Theorem 3eqtr3ri 2850
Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
Hypotheses
Ref Expression
3eqtr3i.1 𝐴 = 𝐵
3eqtr3i.2 𝐴 = 𝐶
3eqtr3i.3 𝐵 = 𝐷
Assertion
Ref Expression
3eqtr3ri 𝐷 = 𝐶

Proof of Theorem 3eqtr3ri
StepHypRef Expression
1 3eqtr3i.3 . 2 𝐵 = 𝐷
2 3eqtr3i.1 . . 3 𝐴 = 𝐵
3 3eqtr3i.2 . . 3 𝐴 = 𝐶
42, 3eqtr3i 2843 . 2 𝐵 = 𝐶
51, 4eqtr3i 2843 1 𝐷 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  indif2  4244  dfif5  4479  resdm2  6081  co01  6107  funiunfv  6998  dfdom2  8523  1mhlfehlf  11844  crreczi  13577  rei  14503  bpoly3  15400  bpoly4  15401  cos1bnd  15528  rpnnen2lem3  15557  rpnnen2lem11  15565  m1bits  15777  6gcd4e2  15874  3lcm2e6  16060  karatsuba  16408  ring1  19281  sincos4thpi  25026  sincos6thpi  25028  1cubrlem  25346  cht3  25677  bclbnd  25783  bposlem8  25794  ex-ind-dvds  28167  ip1ilem  28530  mdexchi  30039  disjxpin  30266  xppreima  30322  df1stres  30365  df2ndres  30366  dpmul100  30500  0dp2dp  30512  dpmul  30516  dpmul4  30517  xrge0slmod  30844  cnrrext  31150  ballotth  31694  hgt750lemd  31818  poimirlem3  34776  poimirlem30  34803  mbfposadd  34820  asindmre  34858  refrelsredund4  35747  sqmid3api  39047  areaquad  39701  inductionexd  40383  stoweidlem26  42188  3exp4mod41  43658
  Copyright terms: Public domain W3C validator