![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq1i | GIF version |
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
eqeq1i | ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | eqeq1 2046 | . 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: ssequn2 3116 dfss1 3141 disj 3268 disjr 3269 undisj1 3279 undisj2 3280 uneqdifeqim 3308 reusn 3441 rabsneu 3443 eusn 3444 iin0r 3922 opeqsn 3989 unisuc 4150 onsucelsucexmid 4255 sucprcreg 4273 onintexmid 4297 dmopab3 4548 dm0rn0 4552 ssdmres 4633 imadisj 4687 args 4694 intirr 4711 dminxp 4765 dfrel3 4778 fntpg 4955 fncnv 4965 dff1o4 5134 dffv4g 5175 fvun2 5240 fnreseql 5277 riota1 5486 riota2df 5488 fnotovb 5548 ovid 5617 ov 5620 ovg 5639 frec0g 5983 diffitest 6344 prarloclem5 6598 renegcl 7272 elznn0 8260 ex-ceil 9896 |
Copyright terms: Public domain | W3C validator |