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

Theorem eqeq2i 2066
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 2065 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 7 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wb 102   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqtri  2076  rabid2  2503  dfss2  2961  equncom  3115  preq12b  3568  preqsn  3573  opeqpr  4017  orddif  4298  dfrel4v  4799  dfiota2  4895  funopg  4961  fnressn  5376  fressnfv  5377  acexmidlemph  5532  fnovim  5636  tpossym  5921  tfr0  5967  qsid  6201  recidpirq  6991  axprecex  7011  negeq0  7327  muleqadd  7722  cjne0  9735  sqrt00  9866  sqrtmsq2i  9961
  Copyright terms: Public domain W3C validator