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 2124 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1316 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: ssequn2 3219 dfss1 3250 disj 3381 disjr 3382 undisj1 3390 undisj2 3391 uneqdifeqim 3418 reusn 3564 rabsneu 3566 eusn 3567 iin0r 4063 opeqsn 4144 unisuc 4305 onsucelsucexmid 4415 sucprcreg 4434 onintexmid 4457 dmopab3 4722 dm0rn0 4726 ssdmres 4811 imadisj 4871 args 4878 intirr 4895 dminxp 4953 dfrel3 4966 fntpg 5149 fncnv 5159 f0rn0 5287 dff1o4 5343 dffv4g 5386 fvun2 5456 fnreseql 5498 riota1 5716 riota2df 5718 fnotovb 5782 ovid 5855 ov 5858 ovg 5877 f1od2 6100 frec0g 6262 diffitest 6749 ismkvnex 6997 prarloclem5 7276 renegcl 7991 elznn0 9037 hashunlem 10518 maxclpr 10962 ex-ceil 12865 nninfsellemqall 13138 nninfomni 13142 |
Copyright terms: Public domain | W3C validator |