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

Theorem eqeq2i 2050
 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 2049 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 7 1 (𝐶 = 𝐴𝐶 = 𝐵)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   = 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:  eqtri  2060  rabid2  2486  dfss2  2934  equncom  3088  preq12b  3541  preqsn  3546  opeqpr  3990  orddif  4271  dfrel4v  4772  dfiota2  4868  funopg  4934  fnressn  5349  fressnfv  5350  acexmidlemph  5505  fnovim  5609  tpossym  5891  tfr0  5937  qsid  6171  recidpirq  6934  axprecex  6954  negeq0  7265  muleqadd  7649  cjne0  9508  sqrt00  9638  sqrtmsq2i  9731
 Copyright terms: Public domain W3C validator