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 2180 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: eqtri 2191 rabid2 2646 dfss2 3136 equncom 3272 preq12b 3755 preqsn 3760 opeqpr 4236 orddif 4529 dfrel4v 5060 dfiota2 5159 funopg 5230 fnressn 5679 fressnfv 5680 acexmidlemph 5843 fnovim 5958 tpossym 6252 qsid 6574 mapsncnv 6669 ixpsnf1o 6710 pw1fin 6884 ss1o0el1o 6886 unfiexmid 6891 onntri35 7201 recidpirq 7807 axprecex 7829 negeq0 8160 muleqadd 8573 fihasheq0 10715 cjne0 10859 sqrt00 10991 sqrtmsq2i 11086 cbvsum 11310 fsump1i 11383 mertenslem2 11486 cbvprod 11508 absefib 11720 efieq1re 11721 lgsdinn0 13664 iswomninnlem 14003 |
Copyright terms: Public domain | W3C validator |