Is this a sufficient proof in the Hilbert Style of $\vdash \neg A \vee (A \wedge B) \equiv \neg A \vee B$?
I'm referencing Distributivity of $\vee$ over $\equiv$ axiom: $A\vee(B\equiv C) \equiv A \vee B \equiv A \vee C$
Proof:
(1) $\neg A \vee ((A \wedge B) \equiv B) \equiv \neg A \vee (A \wedge B) \equiv \neg A \vee B$ (By Distributivity of $\vee$ over $\equiv$ Axiom; 'A-part' is $\neg A$; 'B-Part' is $A\wedge B$; 'C-Part' is $B$)
(2) $\neg A \vee (A \wedge B) \equiv \neg A \vee B \equiv \neg A \vee (A \wedge B) \equiv \neg A \vee B$ (1 + Leibniz; $p \equiv \neg A \vee (A \wedge B) \equiv \neg A \vee B$)
True by previously proven theorem $\vdash A \equiv A$; 'A-part' is $\neg A \vee (A \wedge B) \equiv \neg A \vee B$.
Leibniz (+ Equanimity) application in (2) - 'C-Part' is $p \equiv \neg A \vee (A\wedge B) \equiv \neg A \vee B)$ $$\frac{(\neg A \vee((A\wedge B)\equiv B))\equiv (\neg A \vee (A\wedge B) \equiv \neg A \vee B)}{C[p:=(\neg A \vee ((A\wedge B)\equiv B))]\equiv C[p:=(\neg A \vee (A\wedge B) \equiv \neg A \vee B)}$$