Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqeq2 | Unicode version |
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2171 | . 2 | |
2 | eqcom 2166 | . 2 | |
3 | eqcom 2166 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1342 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: eqeq2i 2175 eqeq2d 2176 eqeq12 2177 eleq1 2227 neeq2 2348 alexeq 2847 ceqex 2848 pm13.183 2859 eqeu 2891 mo2icl 2900 mob2 2901 euind 2908 reu6i 2912 reuind 2926 sbc5 2969 csbiebg 3082 sneq 3581 preqr1g 3740 preqr1 3742 prel12 3745 preq12bg 3747 opth 4209 euotd 4226 ordtriexmid 4492 ontriexmidim 4493 wetriext 4548 tfisi 4558 ideqg 4749 resieq 4888 cnveqb 5053 cnveq0 5054 iota5 5167 funopg 5216 fneq2 5271 foeq3 5402 tz6.12f 5509 funbrfv 5519 fnbrfvb 5521 fvelimab 5536 elrnrexdm 5618 eufnfv 5709 f1veqaeq 5731 mpoeq123 5892 ovmpt4g 5955 ovi3 5969 ovg 5971 caovcang 5994 caovcan 5997 frecabcl 6358 nntri3or 6452 dcdifsnid 6463 nnaordex 6486 nnawordex 6487 ereq2 6500 eroveu 6583 2dom 6762 fundmen 6763 xpf1o 6801 nneneq 6814 tridc 6856 fisseneq 6888 fidcenumlemrks 6909 supsnti 6961 isotilem 6962 updjud 7038 exmidontriimlem3 7170 exmidontriimlem4 7171 onntri35 7184 nqtri3or 7328 ltexnqq 7340 aptisr 7711 srpospr 7715 map2psrprg 7737 axpre-apti 7817 nntopi 7826 subval 8081 eqord1 8372 divvalap 8561 nn0ind-raph 9299 frecuzrdgtcl 10337 frecuzrdgfunlem 10344 sqrtrval 10928 summodclem2 11309 prodmodclem2 11504 divides 11715 dvdstr 11754 odd2np1lem 11794 ndvdssub 11852 eucalglt 11968 hashgcdeq 12150 ennnfonelemim 12300 xmeteq0 12906 trilpo 13763 trirec0 13764 redcwlpo 13775 redc0 13777 reap0 13778 |
Copyright terms: Public domain | W3C validator |