I am trying to work out some basic logic stuff and currently am working with this, given 1 unary operator, denoted $\neg$ and one binary, denoted $\implies$, with the following rules given $$\neg\neg a=a$$ $$a\implies b = \neg b\implies \neg a$$ $$a\implies(b\implies c)=(a\implies b)\implies(a\implies c)$$ $$a=b\implies a$$
I set out to prove the properties of $\land$ and $\lor$ defined as $a\land b=\neg(a\implies \neg b)$ and $a\lor b=\neg a\implies b$. I am working here on purely symbolic manipulations and considering "truth values" now wouldn't sate it because then we are adding some intepritations of this. Of course I am using the ordinary symbols now because it eases reading and shows what my intent is. So please do not go on about truth values.
Now what I have done is proven that $\land$ and $\lor$ are commutative and De Morgans laws, but when I try associative or distributive I am comming to a grinding halt. I have attacked it from left or right parenthesis but can't get it to go anywhere. I got $$(a\lor b)\lor c = \neg(\neg a\implies b)\implies c$$ $$ = \neg c\implies(\neg a\implies b)$$ $$ = (\neg c\implies\neg a)\implies (\neg c\implies b)$$ $$ = (a \implies c)\implies (\neg c\implies b)$$
and quite frankly I don't know where to go here. I might need some smaller lemmas but I don't know which. As said I am trying to build it up from those basics for fun and thinking but I am stuck here.