![]() |
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 2119 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1312 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-4 1468 ax-17 1487 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-cleq 2106 |
This theorem is referenced by: ssequn2 3213 dfss1 3244 disj 3375 disjr 3376 undisj1 3384 undisj2 3385 uneqdifeqim 3412 reusn 3558 rabsneu 3560 eusn 3561 iin0r 4051 opeqsn 4132 unisuc 4293 onsucelsucexmid 4403 sucprcreg 4422 onintexmid 4445 dmopab3 4710 dm0rn0 4714 ssdmres 4797 imadisj 4857 args 4864 intirr 4881 dminxp 4939 dfrel3 4952 fntpg 5135 fncnv 5145 f0rn0 5273 dff1o4 5329 dffv4g 5370 fvun2 5440 fnreseql 5482 riota1 5700 riota2df 5702 fnotovb 5766 ovid 5839 ov 5842 ovg 5861 f1od2 6083 frec0g 6245 diffitest 6731 prarloclem5 7249 renegcl 7939 elznn0 8966 hashunlem 10436 maxclpr 10879 ex-ceil 12618 nninfsellemqall 12888 nninfomni 12892 |
Copyright terms: Public domain | W3C validator |