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

Theorem eqeq2i 2092
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  |-  ( C  =  A  <->  C  =  B )

Proof of Theorem eqeq2i
StepHypRef Expression
1 eqeq2i.1 . 2  |-  A  =  B
2 eqeq2 2091 . 2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
31, 2ax-mp 7 1  |-  ( C  =  A  <->  C  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eqtri  2102  rabid2  2531  dfss2  2989  equncom  3118  preq12b  3564  preqsn  3569  opeqpr  4010  orddif  4292  dfrel4v  4796  dfiota2  4892  funopg  4958  fnressn  5375  fressnfv  5376  acexmidlemph  5530  fnovim  5634  tpossym  5919  qsid  6230  unfiexmid  6428  recidpirq  7077  axprecex  7097  negeq0  7418  muleqadd  7814  sizeeq0  9807  cjne0  9922  sqrt00  10053  sqrtmsq2i  10148
  Copyright terms: Public domain W3C validator