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

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

Proof of Theorem eqeq2i
StepHypRef Expression
1 eqeq2i.1 . 2 A = B
2 eqeq2 2046 . 2 (A = B → (𝐶 = A𝐶 = B))
31, 2ax-mp 7 1 (𝐶 = A𝐶 = B)
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  eqtri  2057  rabid2  2480  dfss2  2928  equncom  3082  preq12b  3532  preqsn  3537  opeqpr  3981  dfrel4v  4715  dfiota2  4811  funopg  4877  fnressn  5292  fressnfv  5293  acexmidlemph  5448  fnovim  5551  tpossym  5832  tfr0  5878  qsid  6107  axprecex  6744  negeq0  7041  muleqadd  7411  cjne0  9116
  Copyright terms: Public domain W3C validator