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 2124 | . 2 | |
2 | eqcom 2119 | . 2 | |
3 | eqcom 2119 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 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: eqeq2i 2128 eqeq2d 2129 eqeq12 2130 eleq1 2180 neeq2 2299 alexeq 2785 ceqex 2786 pm13.183 2796 eqeu 2827 mo2icl 2836 mob2 2837 euind 2844 reu6i 2848 reuind 2862 sbc5 2905 csbiebg 3012 sneq 3508 preqr1g 3663 preqr1 3665 prel12 3668 preq12bg 3670 opth 4129 euotd 4146 ordtriexmid 4407 wetriext 4461 tfisi 4471 ideqg 4660 resieq 4799 cnveqb 4964 cnveq0 4965 iota5 5078 funopg 5127 fneq2 5182 foeq3 5313 tz6.12f 5418 funbrfv 5428 fnbrfvb 5430 fvelimab 5445 elrnrexdm 5527 eufnfv 5616 f1veqaeq 5638 mpoeq123 5798 ovmpt4g 5861 ovi3 5875 ovg 5877 caovcang 5900 caovcan 5903 frecabcl 6264 nntri3or 6357 dcdifsnid 6368 nnaordex 6391 nnawordex 6392 ereq2 6405 eroveu 6488 2dom 6667 fundmen 6668 xpf1o 6706 nneneq 6719 tridc 6761 fisseneq 6788 fidcenumlemrks 6809 supsnti 6860 isotilem 6861 updjud 6935 nqtri3or 7172 ltexnqq 7184 aptisr 7555 srpospr 7559 map2psrprg 7581 axpre-apti 7661 nntopi 7670 subval 7922 eqord1 8213 divvalap 8402 nn0ind-raph 9136 frecuzrdgtcl 10153 frecuzrdgfunlem 10160 sqrtrval 10740 summodclem2 11119 divides 11422 dvdstr 11457 odd2np1lem 11496 ndvdssub 11554 eucalglt 11665 hashgcdeq 11831 ennnfonelemim 11864 xmeteq0 12455 trilpo 13163 |
Copyright terms: Public domain | W3C validator |