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 2147 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1331 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 |
This theorem is referenced by: eqtri 2158 rabid2 2605 dfss2 3081 equncom 3216 preq12b 3692 preqsn 3697 opeqpr 4170 orddif 4457 dfrel4v 4985 dfiota2 5084 funopg 5152 fnressn 5599 fressnfv 5600 acexmidlemph 5760 fnovim 5872 tpossym 6166 qsid 6487 mapsncnv 6582 ixpsnf1o 6623 unfiexmid 6799 recidpirq 7659 axprecex 7681 negeq0 8009 muleqadd 8422 fihasheq0 10533 cjne0 10673 sqrt00 10805 sqrtmsq2i 10900 cbvsum 11122 fsump1i 11195 mertenslem2 11298 cbvprod 11320 absefib 11466 efieq1re 11467 |
Copyright terms: Public domain | W3C validator |