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 2049 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 = wceq 1243 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: eqtri 2060 rabid2 2486 dfss2 2934 equncom 3088 preq12b 3541 preqsn 3546 opeqpr 3990 orddif 4271 dfrel4v 4772 dfiota2 4868 funopg 4934 fnressn 5349 fressnfv 5350 acexmidlemph 5505 fnovim 5609 tpossym 5891 tfr0 5937 qsid 6171 recidpirq 6934 axprecex 6954 negeq0 7265 muleqadd 7649 cjne0 9508 sqrt00 9638 sqrtmsq2i 9731 |
Copyright terms: Public domain | W3C validator |