![]() |
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 2184 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1353 |
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 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: ssequn2 3308 dfss1 3339 disj 3471 disjr 3472 undisj1 3480 undisj2 3481 uneqdifeqim 3508 reusn 3663 rabsneu 3665 eusn 3666 iin0r 4169 opeqsn 4252 unisuc 4413 onsucelsucexmid 4529 sucprcreg 4548 onintexmid 4572 dmopab3 4840 dm0rn0 4844 ssdmres 4929 imadisj 4990 args 4997 intirr 5015 dminxp 5073 dfrel3 5086 fntpg 5272 fncnv 5282 f0rn0 5410 dff1o4 5469 dffv4g 5512 fvun2 5583 fnreseql 5626 riota1 5848 riota2df 5850 fnotovb 5917 ovid 5990 ov 5993 ovg 6012 f1od2 6235 frec0g 6397 diffitest 6886 ismkvnex 7152 prarloclem5 7498 renegcl 8217 elznn0 9267 hashunlem 10783 maxclpr 11230 lgseisenlem1 14386 ex-ceil 14414 nninfsellemqall 14700 nninfomni 14704 iswomni0 14735 |
Copyright terms: Public domain | W3C validator |