Here I have a proposition:

((¬p ∨ x) ∧ (p ∨ y)) → (x ∨ y)

I am proving that it's a tautology but I wanted to know if what I am doing is correct. I'm just learning equivalences, I have tried to type it out as neatly as possible. Please give feedback toward what step are wrong or if there are simpler ways to prove this eq. Yes it took about two hours for me to get this posted. 

≡ ¬[((¬p ∨ x) ∧ (p ∨ y))] ∨ (x ∨ y) implication equivalence

≡ (¬(¬p ∨ x) ∨ ¬(p ∨ y)) ∨ (x ∨ y) DeMorgans

≡ (p ∧ ¬x) ∨ (¬p ∧ ¬y) ∨ (x ∨ y) DeMorgans

≡ [(p ∨ (¬p ∧ ¬y)) ∧ (¬x ∨ (¬p ∧ ¬y))] ∨ (x ∨ y) Distributivity

≡ [(p ∨ ¬p) ∧ (p ∨ ¬y) ∧ (¬x ∨ ¬p) ∧ (¬x ∨ ¬y)] ∨ (x ∨ y) Distributivity

≡ [ T ∧ (p ∨ ¬y) ∧ (¬x ∨ ¬p) ∧ (¬x ∨ ¬y)] ∨ (x ∨ y) Distributivity

≡ [ T ∧ (p ∨ ¬y) ∧ (¬x ∨ ¬p) ∧ (¬x ∨ x)] ∨ (¬y ∨ y) Associativity

≡ [ T ∧ (p ∧ (¬x ∨ ¬p)) ∨ (¬y ∧ (¬x ∨ ¬p))] ∧ T ∨ T Distributivity

≡ [ T ∧ (p ∧ ¬x) ∨ T ∨ (¬y ∧ x) ∨ (¬y ∨ ¬p)] ∧ T Distributivity and Negation law and Idempotent

What do can I do with all these "T"'s in my equation? I'm just going to try to eliminate them.

≡ [(T ∧ T) ∨ (p ∧ ¬x) ∨ (¬y ∧ x) ∨ (¬y ∨ ¬p)] ∧ T Commutative

≡ [T ∨ (p ∧ ¬x) ∨ (¬y ∧ x) ∨ (¬y ∨ ¬p)] ∧ T Idempotent

≡ [T ∨ (p ∨ (¬y ∧ ¬x)) ∧ (¬x ∨ (¬y ∧ ¬x)) ∨ (¬y ∨ ¬p)] ∧ T Distributivity

≡ [T ∨ [(p ∨ ¬y) ∧ (p ∨ ¬x)] ∧ [(¬x ∨ ¬x) ∧ (¬x ∨ ¬y)] ∨ (¬y ∨ ¬p)] ∧ T Distributivity and Commutative

≡ [T ∨ (p ∨ ¬y) ∧ (p ∨ ¬x) ∧ T ∧ (¬x ∨ ¬y) ∧ (¬y ∨ ¬p)] ∧ T Associativity and negation law

≡ [T ∨ (p ∨ ¬y) ∧ (p ∨ ¬x) ∧ T ∧ (¬x ∨ ¬p) ∧ (¬y ∨ ¬y)] ∧ T Associativity

≡ [T ∨ (p ∨ ¬y) ∧ (p ∨ ¬x) ∧ T ∧ (¬x ∨ ¬p)] ∧ T Negation and Idempotent

≡ T ∨ (p ∨ ¬y) ∧ (p ∨ ¬x) ∧ (¬x ∨ ¬p) ∧ T ∧ T Associativity (for the T value)

≡ T ∨ (p ∨ ¬y) ∧ (p ∨ ¬x) ∧ (¬x ∨ ¬p) ∧ T Idempotent

≡ [T ∨ (p ∨ ¬y)] ∧ (¬x ∨ ¬p) ∧ (¬x ∨ p) ∧ T Associativity 

≡ [T ∨ p ∨ ¬y] ∧ (¬x ∨ ¬p) ∧ (¬x ∨ p) ∧ T Associativity 

≡ [(T ∨ ¬y) ∨ p] ∧ (¬x ∨ ¬p) ∧ (¬x ∨ p) ∧ T Associativity 

≡ [T ∨ p] ∧ (¬x ∨ ¬p) ∧ (¬x ∨ p) ∧ T Domination

≡ T ∧ (¬x ∨ ¬p) ∧ (¬x ∨ p) ∧ T Domination

≡ T ∧ T ∧ (¬x ∨ ¬p) ∧ (¬x ∨ p) Associativity

≡ T ∧ (¬x ∨ ¬p) ∧ (¬x ∨ p) Idempotent

≡ T ∧ (¬x ∨ (¬p ∧ p)) Distributivity

≡ T ∧ (¬x ∨ F) Negation

≡ T ∧ ¬x Identity 

≡ ¬x Identity

Great. The wrong answer.