![]() |
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 2106 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqcom 2102 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqcom 2102 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3bitr4g 222 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-4 1455 ax-17 1474 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 |
This theorem is referenced by: eqeq2i 2110 eqeq2d 2111 eqeq12 2112 eleq1 2162 neeq2 2281 alexeq 2765 ceqex 2766 pm13.183 2776 eqeu 2807 mo2icl 2816 mob2 2817 euind 2824 reu6i 2828 reuind 2842 sbc5 2885 csbiebg 2992 sneq 3485 preqr1g 3640 preqr1 3642 prel12 3645 preq12bg 3647 opth 4097 euotd 4114 ordtriexmid 4375 wetriext 4429 tfisi 4439 ideqg 4628 resieq 4765 cnveqb 4930 cnveq0 4931 iota5 5044 funopg 5093 fneq2 5148 foeq3 5279 tz6.12f 5382 funbrfv 5392 fnbrfvb 5394 fvelimab 5409 elrnrexdm 5491 eufnfv 5580 f1veqaeq 5602 mpoeq123 5762 ovmpt4g 5825 ovi3 5839 ovg 5841 caovcang 5864 caovcan 5867 frecabcl 6226 nntri3or 6319 dcdifsnid 6330 nnaordex 6353 nnawordex 6354 ereq2 6367 eroveu 6450 2dom 6629 fundmen 6630 xpf1o 6667 nneneq 6680 tridc 6722 fisseneq 6749 fidcenumlemrks 6769 supsnti 6807 isotilem 6808 updjud 6882 nqtri3or 7105 ltexnqq 7117 aptisr 7474 srpospr 7478 axpre-apti 7570 nntopi 7579 subval 7825 eqord1 8112 divvalap 8295 nn0ind-raph 9020 frecuzrdgtcl 10026 frecuzrdgfunlem 10033 sqrtrval 10612 summodclem2 10990 divides 11290 dvdstr 11325 odd2np1lem 11364 ndvdssub 11422 eucalglt 11531 hashgcdeq 11696 ennnfonelemim 11729 xmeteq0 12287 trilpo 12820 |
Copyright terms: Public domain | W3C validator |