# Proving a biconditional statement with an or

I want to prove a theorem in geometry of the form $p \iff q \vee r$. My plan is to prove:

1. $q \implies p$ as well as $r \implies p$
2. $p \text{ and } \lnot q \implies r$

Can I get someone to verify that I haven't sidetracked in my logic?

The following calculation shows that your logic is fine: \begin{align} & p \iff q \lor r \\ \iff & \;\;\;\;\;\text{"split $\iff$ into both directions"} \\ & (p \implies q \lor r) \;\land\; (q \lor r \implies p) \\ \iff & \;\;\;\;\;\text{"expand $\implies$, twice; use De Morgan in RHS"} \\ & (\lnot p \lor q \lor r) \;\land\; ((\lnot q \land \lnot r) \lor p) \\ \iff & \;\;\;\;\;\text{"distribute $\lor$ over $\land$ in RHS"} \\ & (\lnot p \lor q \lor r) \;\land\; (\lnot q \lor p) \;\land\; (\lnot r \lor p) \\ \iff & \;\;\;\;\;\text{"introduce $\implies$ again, three times, using De Morgan for the first time"} \\ & (p \land \lnot q \implies r) \;\land\; (q \implies p) \;\land\; (r \implies p) \\ \end{align}