Prove that a formula in propositional logic depends only on a subset of variables I have the following equality in propositional logic:
(p ∨ q) ∧ (r ∨ p) ∧ (¬q ∨ ¬r ∨ p) ≡ p

and I want to prove it without using its thruth table. My intuition is that the equality holds because the result only depends on p: Whatever value q/r takes, it will appear both the value itself and negated, therefore the whole formula will be never satisfiable unless we use p.
Is there any way to give a more formal proof of that?
 A: You can just evaluate the statement filling in either value of $p$.
So, if $P = T$:
$(T \lor q) \land (r \lor T) \land (¬q \lor ¬r \lor T) ≡ T \land T \land T ≡ T$  Check!
If $p = F$:
$(F \lor q) \land (r \lor F) \land (¬q \lor ¬r \lor F) \equiv q \land r  \land (¬q \lor ¬r) \equiv (q \land r)  \land ¬(q \land r) \equiv F$ Check!
A: Your intuition is spot on.  But we don't need to prove so using a truth-table or otherwise assigning truth values to any of the variable to check the equivalence.
We don't have to do so because we can prove the equivalence without knowing  all possible truth value assignments.
Below, in only one step, is "false" used, and that's when we  have something of the form $a \land \lnot a$, which is a contradiction, thus always false.
Okay, let's look at the claim to be proven:

$$(\color{blue}{p} \lor q) \land (r \lor \color{blue}{p}) \land (¬q \lor ¬r \lor \color{blue}{p}) \equiv p\tag{ * }$$

Let's work on the left-hand side of $(*)$, to simplify it:
We see that $\color{blue}{p}$ is a disjunct in  all three of the clauses we start with on the left-hand-side,  so we can write an equivalent statement by "reverse" distribution, which is in fact justified by distributivity of $\lor$ over $\land$ which is two-directional:  $$a\lor (b \land c \land d) \iff  (a \lor b)\land (a \lor c) \land (a \lor d)\tag{e.g., distribution}$$ Now, we  apply this to to the left-hand-side of $(*)$to get:

$$(\color{blue} p \lor q) \land (\color{blue}p \lor r) \land (¬q \lor ¬r \lor \color{blue}p) \equiv \color{blue}p\lor(q \land r \land (\lnot q \lor \lnot r))$$

Now, using Demorgans's on the last term, we get $\lnot q \lor \lnot r \equiv \lnot(q \land r)$.  This brings us to a contradiction in one of the disjuncts:

$$\equiv p\lor \underbrace{((q \land r) \land \lnot (q \land r))}_{\large{\bot} \;\text{contradiction}}$$
$$\equiv p\lor F $$
$$\equiv p$$

So we have the left hand side equivalent to the right hand side: $p \equiv p$
A: The OP asks:

Is there any way to give a more formal proof of that?

Here is a natural deduction proof using a Fitch-style proof checker:


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
