![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq2 | GIF version |
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq2 | ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2196 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | eqcom 2191 | . 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶) | |
3 | eqcom 2191 | . 2 ⊢ (𝐶 = 𝐵 ↔ 𝐵 = 𝐶) | |
4 | 1, 2, 3 | 3bitr4g 223 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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: eqeq2i 2200 eqeq2d 2201 eqeq12 2202 eleq1 2252 neeq2 2374 alexeq 2878 ceqex 2879 pm13.183 2890 eqeu 2922 mo2icl 2931 mob2 2932 euind 2939 reu6i 2943 reuind 2957 sbc5 3001 csbiebg 3114 sneq 3618 preqr1g 3781 preqr1 3783 prel12 3786 preq12bg 3788 opth 4252 euotd 4269 ordtriexmid 4535 ontriexmidim 4536 wetriext 4591 tfisi 4601 ideqg 4793 resieq 4932 cnveqb 5099 cnveq0 5100 iota5 5214 funopg 5266 fneq2 5321 foeq3 5452 tz6.12f 5560 funbrfv 5571 fnbrfvb 5573 fvelimab 5589 elrnrexdm 5672 eufnfv 5764 f1veqaeq 5787 mpoeq123 5951 ovmpt4g 6015 ovi3 6029 ovg 6031 caovcang 6054 caovcan 6057 frecabcl 6419 nntri3or 6513 dcdifsnid 6524 nnaordex 6548 nnawordex 6549 ereq2 6562 eroveu 6647 2dom 6826 fundmen 6827 xpf1o 6867 nneneq 6880 tridc 6922 fisseneq 6955 fidcenumlemrks 6977 supsnti 7029 isotilem 7030 updjud 7106 nninfwlpoimlemdc 7200 exmidontriimlem3 7247 exmidontriimlem4 7248 onntri35 7261 exmidapne 7284 nqtri3or 7420 ltexnqq 7432 aptisr 7803 srpospr 7807 map2psrprg 7829 axpre-apti 7909 nntopi 7918 subval 8174 eqord1 8465 divvalap 8656 nn0ind-raph 9395 frecuzrdgtcl 10438 frecuzrdgfunlem 10445 sqrtrval 11036 summodclem2 11417 prodmodclem2 11612 divides 11823 dvdstr 11862 odd2np1lem 11904 ndvdssub 11962 eucalglt 12084 hashgcdeq 12266 ennnfonelemim 12470 imasaddfnlemg 12784 dfgrp2 12964 grpidinv 12996 dfgrp3mlem 13035 xmeteq0 14296 trilpo 15229 trirec0 15230 redcwlpo 15241 redc0 15243 reap0 15244 |
Copyright terms: Public domain | W3C validator |