![]() |
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 | ⊢ A = B |
Ref | Expression |
---|---|
eqeq1i | ⊢ (A = 𝐶 ↔ B = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1i.1 | . 2 ⊢ A = B | |
2 | eqeq1 2043 | . 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (A = 𝐶 ↔ B = 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 = wceq 1242 |
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 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: ssequn2 3110 dfss1 3135 disj 3262 disjr 3263 undisj1 3273 undisj2 3274 uneqdifeqim 3302 reusn 3432 rabsneu 3434 eusn 3435 iin0r 3913 opeqsn 3980 unisuc 4116 onsucelsucexmid 4215 sucprcreg 4227 dmopab3 4491 dm0rn0 4495 ssdmres 4576 imadisj 4630 args 4637 intirr 4654 dminxp 4708 dfrel3 4721 fntpg 4898 fncnv 4908 dff1o4 5077 dffv4g 5118 fvun2 5183 fnreseql 5220 riota1 5429 riota2df 5431 fnotovb 5490 ovid 5559 ov 5562 ovg 5581 frec0g 5922 prarloclem5 6483 renegcl 7068 elznn0 8036 |
Copyright terms: Public domain | W3C validator |