![]() |
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 2098 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1290 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-4 1446 ax-17 1465 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 |
This theorem is referenced by: eqtri 2109 rabid2 2544 dfss2 3015 equncom 3146 preq12b 3620 preqsn 3625 opeqpr 4089 orddif 4376 dfrel4v 4895 dfiota2 4994 funopg 5061 fnressn 5497 fressnfv 5498 acexmidlemph 5659 fnovim 5767 tpossym 6055 qsid 6371 mapsncnv 6466 ixpsnf1o 6507 unfiexmid 6682 recidpirq 7456 axprecex 7476 negeq0 7797 muleqadd 8198 fihasheq0 10263 cjne0 10403 sqrt00 10534 sqrtmsq2i 10629 cbvsum 10810 fsump1i 10888 mertenslem2 10991 absefib 11121 efieq1re 11122 |
Copyright terms: Public domain | W3C validator |