The symbol (called "turnstile", maybe because it looks like a turnstile in the subway) separates assumptions from conclusions. For example, is a correct statement. In your example, there are no assumptions.

Judging by Axioms for propositional logic E, The Golden Rule is "p /\ q == p == q == p \/ q". We instantiate p = A and q = A V B to getA ^ (AVB)

By Golden Rule

=> A A V B A V A V B

Now, is what we need to show. So, the right-hand side is rewritten as by the idempotency of disjunction. So we get , which can be rewritten to .

With all due respect to D. Gries, this formulation of propositional logic seems curious but eccentric; I have not seen any serious logician using it these years.