Proving equivalences 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. 
 A: There are different methods to solve this problem from propositional logic. One should use always use paranthese to avoid expressions like
$$a \lor b \land c$$
Does this mean
$$(a \lor b) \land c$$
because $\lor$ has higher precedence than $\land$ or because they have euqal precedence and the expressions is evaluated from left to right? Or is it
$$ a \lor (b \land c)$$
because $\land$ has higher precedence than $\lor$ or because they have equal precedence and the expressions is evaluated from right to left?
The latter is the case because $\land$ has a higher precedence than $\lor$.
Using this precedence rules the following lines of your proof are wrong
  T ∨ (p ∨ ¬y) ∧ (p ∨ ¬x) ∧ (¬x ∨ ¬p) ∧ T Idempotent

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

Deduction
I use the laws of Boolean algebra
$$\begin{eqnarray} 
&& ((\lnot p \lor x) \land (p \lor y)) \to (x \lor y)   \\
&\equiv & \lnot ((\lnot p \lor x) \land (p \lor y)) \lor (x \lor y) & \text{implication equivalence}\\
&\equiv &  (\lnot(\lnot p \lor x) \lor \lnot (p \lor y)) \lor (x \lor y) & \text{DeMorgan}\\
&\equiv &  ((\lnot(\lnot p) \land \lnot x) \lor (\lnot p \land \lnot y)) \lor (x \lor y) & \text{DeMorgan}\\
&\equiv &  ((p \land \lnot x) \lor  (\lnot p \land \lnot y)) \lor (x \lor y) & \text{Double negation}\\
&\equiv &  (p \land \lnot x) \lor  (\lnot p \land \lnot y) \lor x \lor y & \text{Associativity}\\
&\equiv &  ((p \land \lnot x) \lor x) \lor ((\lnot p \land \lnot y)  \lor y )& \text{Commutativity and Associatvity}\\
&\equiv &  ((p \lor x) \land (\lnot x \lor x) ) \lor ((\lnot p \lor y) \land (\lnot y \lor y)   )& \text{Distributivity}\\
&\equiv &  ((p \lor x) \land T ) \lor ((\lnot p \lor y) \land T  ) & \text{Complementation}\\
&\equiv &  (p \lor x)  \lor (\lnot p \lor y ) & \text{Identity}\\
&\equiv &  (p \lor x  \lor \lnot p \lor y ) & \text{Associativity}\\
&\equiv &  ((p \lor \lnot p) \lor x  \lor y ) &\text{Commutativity and Associativity}\\
&\equiv &  (T \lor x  \lor y ) & \text{Complementation}\\
&\equiv &  ((T \lor x ) \lor y ) & \text{Associativity}\\
&\equiv &  (T\lor y ) & \text{Annihilator}\\
&\equiv &  T\ & \text{Annihilator}\\
\end{eqnarray} 
$$
Using a truth table
I use $0$ and $1$ instead of $F$ and $T$. This is easier to read in the following truth table
$$
\begin{array}{c}
p&x&y&\lnot p&\lnot p \lor x&p \lor y&(\lnot p \lor x) \land (p \lor y)&x \lor y&((\lnot p \lor x) \land (p \lor y)) \to (x \lor y)\\
\hline\\
0&0&0&1&1&0&0&0&1\\
0&0&1&1&1&1&1&1&1\\
0&1&0&1&1&0&0&1&1\\
0&1&1&1&1&1&1&1&1\\
1&0&0&0&0&1&0&0&1\\
1&0&1&0&0&1&0&1&1\\
1&1&0&0&1&1&1&1&1\\
1&1&1&0&1&1&1&1&1\\
\end{array}
$$
A: It has to be said, this is a crazy way to go about establishing the given wff is a tautology. A brute force truth-table would be very much quicker and (evidently!) more fool-proof.
For note that the conditional ((¬p ∨ x) ∧ (p ∨ y)) → (x ∨ y) is true whenever the consequent (x ∨ y) is true, which is on six of the eight lines of the truth-table. So you only have to do any more working on two lines, and job done!
A tautology is, by definition, a formula which is true on all valuations of its atoms -- so a brute force truth-table (looking at every valuation and seeing if the formula is true) has to be the most direct method of checking. Not always the quickest, to be sure. By all means, then, use short-cuts (e.g. use known equivalences), or "work backwards" (using tableaux) if that cuts down the necessary working. But it isn't very smart to use those other methods if they make more work than a direct assault!!
A: $$\begin{align}
((\neg p \vee x)\wedge(p\vee y))\rightarrow(x\vee y)
\equiv& \neg((\neg p \vee x)\wedge(p\vee y))\vee(x\vee y)\\
\equiv& (\neg(\neg p\vee x)\vee\neg(p\vee y)) \vee (x\vee y)\\
\equiv& ((p\wedge\neg x)\vee(\neg p\wedge \neg y)) \vee (x\vee y)\\
\equiv& (p\wedge\neg x)\vee(\neg p\wedge \neg y) \vee x\vee y\\
\equiv& (p\wedge\neg x)\vee(\neg p\wedge \neg y) \vee (T\wedge x)\vee (T\wedge y)\\
\equiv& (p\wedge\neg x)\vee(\neg p\wedge \neg y) \vee ((p\vee T)\wedge x)\vee ((\neg p\vee T)\wedge y)\\
\equiv& (p\wedge\neg x)\vee(\neg p\wedge \neg y) \vee (p\wedge x)\vee(T\wedge x)\vee (\neg p\wedge y) \vee(T\wedge y)\\
\equiv& (p\wedge\neg x) \vee (p\wedge x)\vee(\neg p\wedge \neg y)\vee (\neg p\wedge y)\vee(T\wedge x) \vee(T\wedge y)\\
\equiv& (p\wedge(\neg x\vee x))\vee(\neg p\wedge(\neg y\vee y))\vee(T\wedge x) \vee(T\wedge y)\\
\equiv& (p\wedge T)\vee(\neg p\wedge T)\vee(T\wedge x) \vee(T\wedge y)\\
\equiv& p\vee\neg p\vee x\vee y\\
\equiv& T\vee x \vee y\\
\equiv& T
\end{align}$$
A: Suppose p=0.  Then we have:
[((¬0 ∨ x) ∧ (0 ∨ y)) → (x ∨ y)]=[(1 ∨ x)∧ (0 ∨ y)) → (x ∨ y)].
=[(1 ∨ x)∧ (0 ∨ y)) → (x ∨ y)]=[(1∧y)→ (x ∨ y)] since (1 $\lor$ x)=1, and (0∨y)=y.
[(1∧y)→ (x ∨ y)]=[y→(x ∨ y)], which can get read "if y, then x or y".  So, this case holds.
Suppose p=1. Then we have:
[[((¬1 ∨ x) ∧ (1 ∨ y)) → (x ∨ y)]=[[((0 ∨ x) ∧ (1 ∨ y)) → (x ∨ y)].
[[((0 ∨ x) ∧ (1 ∨ y)) → (x ∨ y)]=[(x$\land$1)→ (x ∨ y)]. (see the above).
[(x$\land$1)→ (x ∨ y)]=[x→ (x ∨ y)], which can get read "if x, then x or y".  So, this case holds.
Since the above two cases covers all cases, it holds in all cases.
If you have more than two truth values you only need to change 0 to "falsum" here and "1" to "verum", the identities used still work.  The "if x, then x or y" and "if y, then x or y" statements would need checked more thoroughly in such a case, but that won't end up posing a problem.
