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 2046 | . 2 | |
2 | eqcom 2042 | . 2 | |
3 | eqcom 2042 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 212 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 wceq 1243 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: eqeq2i 2050 eqeq2d 2051 eqeq12 2052 eleq1 2100 neeq2 2219 alexeq 2670 ceqex 2671 pm13.183 2681 eqeu 2711 mo2icl 2720 mob2 2721 euind 2728 reu6i 2732 reuind 2744 sbc5 2787 csbiebg 2889 sneq 3386 preqr1g 3537 preqr1 3539 prel12 3542 preq12bg 3544 opth 3974 euotd 3991 ordtriexmid 4247 wetriext 4301 tfisi 4310 ideqg 4487 resieq 4622 cnveqb 4776 cnveq0 4777 iota5 4887 funopg 4934 fneq2 4988 foeq3 5104 tz6.12f 5202 funbrfv 5212 fnbrfvb 5214 fvelimab 5229 elrnrexdm 5306 eufnfv 5389 f1veqaeq 5408 mpt2eq123 5564 ovmpt4g 5623 ovi3 5637 ovg 5639 caovcang 5662 caovcan 5665 nntri3or 6072 nnaordex 6100 nnawordex 6101 ereq2 6114 eroveu 6197 2dom 6285 fundmen 6286 nneneq 6320 nqtri3or 6494 ltexnqq 6506 aptisr 6863 srpospr 6867 axpre-apti 6959 nntopi 6968 subval 7203 divvalap 7653 nn0ind-raph 8355 frecuzrdgfn 9198 sqrtrval 9598 |
Copyright terms: Public domain | W3C validator |