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

Theorem eqtr2i 2374
 Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1 A = B
eqtr2i.2 B = C
Assertion
Ref Expression
eqtr2i C = A

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3 A = B
2 eqtr2i.2 . . 3 B = C
31, 2eqtri 2373 . 2 A = C
43eqcomi 2357 1 C = A
 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:  3eqtrri  2378  3eqtr2ri  2380  dfun3  3493  symdif1  3519  iunin  3547  iinun  3548  dfif3  3672  dfsn2  3747  ssunpr  3868  sstp  3870  tfinnn  4534  xpindi  4864  xpindir  4865  foimacnv  5303  clos1base  5878  pmex  6005  fundmen  6043  nncdiv3  6277  nnc3p1n3p2  6280  nchoicelem1  6289
 Copyright terms: Public domain W3C validator