New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3eqtr3i GIF version

Theorem 3eqtr3i 2381
 Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3i.1 A = B
3eqtr3i.2 A = C
3eqtr3i.3 B = D
Assertion
Ref Expression
3eqtr3i C = D

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3 A = B
2 3eqtr3i.2 . . 3 A = C
31, 2eqtr3i 2375 . 2 B = C
4 3eqtr3i.3 . 2 B = D
53, 4eqtr3i 2375 1 C = D
 Colors of variables: wff setvar class Syntax hints:   = wceq 1642 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346 This theorem is referenced by:  csbvarg  3163  un12  3421  in12  3466  indif1  3499  difundi  3507  difundir  3508  difindi  3509  difindir  3510  dif32  3517  undif1  3625  addc4  4417  addc6  4418  tfin1c  4499  xp0  5044  caov12  5636  caov13  5638  caov411  5640  caovdir  5642  tcdi  6164  tc2c  6166  ce0addcnnul  6179  nchoicelem1  6289
 Copyright terms: Public domain W3C validator