![]() |
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 2196 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1364 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: ssequn2 3323 dfss1 3354 disj 3486 disjr 3487 undisj1 3495 undisj2 3496 uneqdifeqim 3523 reusn 3678 rabsneu 3680 eusn 3681 iin0r 4187 opeqsn 4270 unisuc 4431 onsucelsucexmid 4547 sucprcreg 4566 onintexmid 4590 dmopab3 4858 dm0rn0 4862 ssdmres 4947 imadisj 5008 args 5015 intirr 5033 dminxp 5091 dfrel3 5104 fntpg 5291 fncnv 5301 f0rn0 5429 dff1o4 5488 dffv4g 5531 fvun2 5604 fnreseql 5647 riota1 5871 riota2df 5873 fnotovb 5940 ovid 6014 ov 6017 ovg 6036 f1od2 6261 frec0g 6423 diffitest 6916 ismkvnex 7184 prarloclem5 7530 renegcl 8249 elznn0 9299 hashunlem 10819 maxclpr 11266 lgseisenlem1 14928 ex-ceil 14956 nninfsellemqall 15243 nninfomni 15247 iswomni0 15278 |
Copyright terms: Public domain | W3C validator |