Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqeq2i | Unicode version |
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq2i.1 |
Ref | Expression |
---|---|
eqeq2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2i.1 | . 2 | |
2 | eqeq2 2174 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wceq 1342 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: eqtri 2185 rabid2 2640 dfss2 3126 equncom 3262 preq12b 3744 preqsn 3749 opeqpr 4225 orddif 4518 dfrel4v 5049 dfiota2 5148 funopg 5216 fnressn 5665 fressnfv 5666 acexmidlemph 5829 fnovim 5941 tpossym 6235 qsid 6557 mapsncnv 6652 ixpsnf1o 6693 pw1fin 6867 ss1o0el1o 6869 unfiexmid 6874 onntri35 7184 recidpirq 7790 axprecex 7812 negeq0 8143 muleqadd 8556 fihasheq0 10696 cjne0 10836 sqrt00 10968 sqrtmsq2i 11063 cbvsum 11287 fsump1i 11360 mertenslem2 11463 cbvprod 11485 absefib 11697 efieq1re 11698 iswomninnlem 13769 |
Copyright terms: Public domain | W3C validator |