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

Theorem eqtr3d 2387
 Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr3d.1 (φA = B)
eqtr3d.2 (φA = C)
Assertion
Ref Expression
eqtr3d (φB = C)

Proof of Theorem eqtr3d
StepHypRef Expression
1 eqtr3d.1 . . 3 (φA = B)
21eqcomd 2358 . 2 (φB = A)
3 eqtr3d.2 . 2 (φA = C)
42, 3eqtrd 2385 1 (φB = C)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = 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:  3eqtr3d  2393  3eqtr3rd  2394  3eqtr3a  2409  uniintsn  3963  f00  5249  f1imacnv  5302  foimacnv  5303  fvsnun2  5448  oprssov  5603  caovmo  5645  fvfullfunlem3  5863  ecss  5966  uniqs2  5985  map0b  6024  enprmaplem3  6078  ncdisjun  6136  ncspw1eu  6159  addcdi  6250  nchoicelem17  6305
 Copyright terms: Public domain W3C validator