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

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

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3 A = B
2 eqtr2i.2 . . 3 B = 𝐶
31, 2eqtri 2057 . 2 A = 𝐶
43eqcomi 2041 1 𝐶 = A
 Colors of variables: wff set class Syntax hints:   = wceq 1242 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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-cleq 2030 This theorem is referenced by:  3eqtrri  2062  3eqtr2ri  2064  symdif1  3196  dfif3  3337  dfsn2  3381  prprc1  3469  ruv  4228  xpindi  4414  xpindir  4415  dmcnvcnv  4501  rncnvcnv  4502  imainrect  4709  dfrn4  4724  fcoi1  5013  foimacnv  5087  fsnunfv  5306  dfoprab3  5759  pitonnlem1  6741  ixi  7367  recexaplem2  7415  zeo  8119  num0h  8153  dec10p  8172  fseq1p1m1  8726
 Copyright terms: Public domain W3C validator