Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqtr2i GIF version

Theorem eqtr2i 2061
 Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1 𝐴 = 𝐵
eqtr2i.2 𝐵 = 𝐶
Assertion
Ref Expression
eqtr2i 𝐶 = 𝐴

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3 𝐴 = 𝐵
2 eqtr2i.2 . . 3 𝐵 = 𝐶
31, 2eqtri 2060 . 2 𝐴 = 𝐶
43eqcomi 2044 1 𝐶 = 𝐴
 Colors of variables: wff set class Syntax hints:   = wceq 1243 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  3eqtrri  2065  3eqtr2ri  2067  symdif1  3202  dfif3  3343  dfsn2  3389  prprc1  3478  ruv  4274  xpindi  4471  xpindir  4472  dmcnvcnv  4558  rncnvcnv  4559  imainrect  4766  dfrn4  4781  fcoi1  5070  foimacnv  5144  fsnunfv  5363  dfoprab3  5817  pitonnlem1  6921  ixi  7574  recexaplem2  7633  zeo  8343  num0h  8377  dec10p  8396  fseq1p1m1  8956
 Copyright terms: Public domain W3C validator