![]() |
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 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: ![]() ![]() ![]() |
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 4255 euotd 4272 ordtriexmid 4538 ontriexmidim 4539 wetriext 4594 tfisi 4604 ideqg 4796 resieq 4935 cnveqb 5102 cnveq0 5103 iota5 5217 funopg 5269 fneq2 5324 foeq3 5455 tz6.12f 5563 funbrfv 5574 fnbrfvb 5576 fvelimab 5592 elrnrexdm 5675 eufnfv 5767 f1veqaeq 5790 mpoeq123 5954 ovmpt4g 6018 ovi3 6032 ovg 6034 caovcang 6057 caovcan 6060 frecabcl 6423 nntri3or 6517 dcdifsnid 6528 nnaordex 6552 nnawordex 6553 ereq2 6566 eroveu 6651 2dom 6830 fundmen 6831 xpf1o 6871 nneneq 6884 tridc 6926 fisseneq 6959 fidcenumlemrks 6981 supsnti 7033 isotilem 7034 updjud 7110 nninfwlpoimlemdc 7204 exmidontriimlem3 7251 exmidontriimlem4 7252 onntri35 7265 exmidapne 7288 nqtri3or 7424 ltexnqq 7436 aptisr 7807 srpospr 7811 map2psrprg 7833 axpre-apti 7913 nntopi 7922 subval 8178 eqord1 8469 divvalap 8660 nn0ind-raph 9399 frecuzrdgtcl 10442 frecuzrdgfunlem 10449 sqrtrval 11040 summodclem2 11421 prodmodclem2 11616 divides 11827 dvdstr 11866 odd2np1lem 11908 ndvdssub 11966 eucalglt 12088 hashgcdeq 12270 ennnfonelemim 12474 imasaddfnlemg 12788 dfgrp2 12968 grpidinv 13000 dfgrp3mlem 13039 xmeteq0 14311 trilpo 15245 trirec0 15246 redcwlpo 15257 redc0 15259 reap0 15260 |
Copyright terms: Public domain | W3C validator |