![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq2i | GIF 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 2187 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: eqtri 2198 rabid2 2654 dfss2 3146 equncom 3282 preq12b 3772 preqsn 3777 opeqpr 4255 orddif 4548 dfrel4v 5082 dfiota2 5181 funopg 5252 fnressn 5704 fressnfv 5705 acexmidlemph 5870 fnovim 5985 tpossym 6279 qsid 6602 mapsncnv 6697 ixpsnf1o 6738 pw1fin 6912 ss1o0el1o 6914 unfiexmid 6919 onntri35 7238 recidpirq 7859 axprecex 7881 negeq0 8213 muleqadd 8627 fihasheq0 10775 cjne0 10919 sqrt00 11051 sqrtmsq2i 11146 cbvsum 11370 fsump1i 11443 mertenslem2 11546 cbvprod 11568 absefib 11780 efieq1re 11781 isnsg4 13077 lgsdinn0 14534 m1lgs 14537 iswomninnlem 14882 |
Copyright terms: Public domain | W3C validator |