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

Theorem eqeq2i 2181
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 2180 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1348
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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163
This theorem is referenced by:  eqtri  2191  rabid2  2646  dfss2  3136  equncom  3272  preq12b  3755  preqsn  3760  opeqpr  4236  orddif  4529  dfrel4v  5060  dfiota2  5159  funopg  5230  fnressn  5679  fressnfv  5680  acexmidlemph  5843  fnovim  5958  tpossym  6252  qsid  6574  mapsncnv  6669  ixpsnf1o  6710  pw1fin  6884  ss1o0el1o  6886  unfiexmid  6891  onntri35  7201  recidpirq  7807  axprecex  7829  negeq0  8160  muleqadd  8573  fihasheq0  10715  cjne0  10859  sqrt00  10991  sqrtmsq2i  11086  cbvsum  11310  fsump1i  11383  mertenslem2  11486  cbvprod  11508  absefib  11720  efieq1re  11721  lgsdinn0  13664  iswomninnlem  14003
  Copyright terms: Public domain W3C validator