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

Theorem eqtr2i 2226
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 2225 . 2 𝐴 = 𝐶
43eqcomi 2208 1 𝐶 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186
This theorem depends on definitions:  df-bi 117  df-cleq 2197
This theorem is referenced by:  3eqtrri  2230  3eqtr2ri  2232  symdif1  3437  dfif3  3583  dfsn2  3646  prprc1  3740  ruv  4597  xpindi  4812  xpindir  4813  dmcnvcnv  4901  rncnvcnv  4902  imainrect  5127  dfrn4  5142  fcoi1  5455  foimacnv  5539  fsnunfv  5784  dfoprab3  6276  fiintim  7027  sbthlemi8  7065  pitonnlem1  7957  ixi  8655  recexaplem2  8724  zeo  9477  num0h  9514  dec10p  9545  fseq1p1m1  10215  fsumrelem  11724  ef0lem  11913  ef01bndlem  12009  3lcm2e6woprm  12350  strsl0  12823  0g0  13150  tgioo  14968  tgqioo  14969  dveflem  15140  sincos4thpi  15254  coskpi  15262
  Copyright terms: Public domain W3C validator