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

Theorem eqeq2i 2150
 Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqeq2i.1 𝐴 = 𝐵
Assertion
Ref Expression
eqeq2i (𝐶 = 𝐴𝐶 = 𝐵)

Proof of Theorem eqeq2i
StepHypRef Expression
1 eqeq2i.1 . 2 𝐴 = 𝐵
2 eqeq2 2149 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   = 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:  eqtri  2160  rabid2  2607  dfss2  3086  equncom  3221  preq12b  3697  preqsn  3702  opeqpr  4175  orddif  4462  dfrel4v  4990  dfiota2  5089  funopg  5157  fnressn  5606  fressnfv  5607  acexmidlemph  5767  fnovim  5879  tpossym  6173  qsid  6494  mapsncnv  6589  ixpsnf1o  6630  unfiexmid  6806  recidpirq  7673  axprecex  7695  negeq0  8023  muleqadd  8436  fihasheq0  10547  cjne0  10687  sqrt00  10819  sqrtmsq2i  10914  cbvsum  11136  fsump1i  11209  mertenslem2  11312  cbvprod  11334  absefib  11484  efieq1re  11485
 Copyright terms: Public domain W3C validator