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

Theorem eqtr2i 2161
 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 2160 . 2 𝐴 = 𝐶
43eqcomi 2143 1 𝐶 = 𝐴
 Colors of variables: wff set class Syntax hints:   = wceq 1331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  3eqtrri  2165  3eqtr2ri  2167  symdif1  3341  dfif3  3487  dfsn2  3541  prprc1  3631  ruv  4465  xpindi  4674  xpindir  4675  dmcnvcnv  4763  rncnvcnv  4764  imainrect  4984  dfrn4  4999  fcoi1  5303  foimacnv  5385  fsnunfv  5621  dfoprab3  6089  fiintim  6817  sbthlemi8  6852  pitonnlem1  7665  ixi  8357  recexaplem2  8425  zeo  9168  num0h  9205  dec10p  9236  fseq1p1m1  9886  fsumrelem  11252  ef0lem  11378  ef01bndlem  11474  3lcm2e6woprm  11778  strsl0  12021  tgioo  12729  tgqioo  12730  dveflem  12870  sincos4thpi  12943  coskpi  12951
 Copyright terms: Public domain W3C validator