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

Theorem eqeq2i 2151
 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 2150 . 2
31, 2ax-mp 5 1
 Colors of variables: wff set class Syntax hints:   wb 104   wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  eqtri  2161  rabid2  2610  dfss2  3091  equncom  3226  preq12b  3705  preqsn  3710  opeqpr  4183  orddif  4470  dfrel4v  4998  dfiota2  5097  funopg  5165  fnressn  5614  fressnfv  5615  acexmidlemph  5775  fnovim  5887  tpossym  6181  qsid  6502  mapsncnv  6597  ixpsnf1o  6638  unfiexmid  6814  recidpirq  7691  axprecex  7713  negeq0  8041  muleqadd  8454  fihasheq0  10573  cjne0  10713  sqrt00  10845  sqrtmsq2i  10940  cbvsum  11162  fsump1i  11235  mertenslem2  11338  cbvprod  11360  absefib  11514  efieq1re  11515  iswomninnlem  13418
 Copyright terms: Public domain W3C validator