avewright/proofwiki-math huggingface dataset:
Theorem: De Morgan's Laws (Logic)/Conjunction/Formulation 2

:$\vdash \paren {p \land q} \iff \paren {\neg \paren {\neg p \lor \neg q} }$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
$\begin{array}{|ccc|c|cccccc|} \hline
(p & \land & q) & \iff & (\neg & (\neg & p & \lor & \neg & q))  \\
\hline
\F & \F & \F & \T & \F & \T & \F & \T & \T & \F \\
\F & \F & \T & \T & \F & \T & \F & \T & \F & \T \\
\T & \F & \F & \T & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: De Morgan's Laws (Logic)/Disjunction/Formulation 2

:$\vdash \paren {p \lor q} \iff \paren {\neg \paren {\neg p \land \neg q} }$

Proof:
{{BeginTableau|\vdash \paren {p \lor q} \iff \paren {\neg \paren {\neg p \land \neg q} } }}
{{Assumption|1|p \lor q}}
{{SequentIntro|2|1|\neg \paren {\neg p \land \neg q}|1|De Morgan's Laws (Logic): Disjunction: Formulation 1}}
{{Implication|3||\paren {p \lor q} \implies \paren {\neg \paren {\neg p \land \neg q} }|1|2}}
{{Assumption|4|\neg \paren {\neg p \land \neg q} }}
{{SequentIntro|5|4|p \lor q|4|De Morgan's Laws (Logic): Disjunction: Formulation 1}}
{{Implication|6||\paren {\neg \paren {\neg p \land \neg q} } \implies \paren {p \lor q}|4|5}}
{{BiconditionalIntro|7||\paren {p \lor q} \iff \paren {\neg \paren {\neg p \land \neg q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: De Morgan's Laws (Logic)/Disjunction/Formulation 2

:$\vdash \paren {p \lor q} \iff \paren {\neg \paren {\neg p \land \neg q} }$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|cccccc|} \hline
(p & \lor & q) & \iff & (\neg & (\neg & p & \land & \neg & q)) \\
\hline
\F & \F & \F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \F & \T & \T & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws (Logic)/Disjunction/Formulation 1/Forward Implication

:$p \lor q \vdash \neg \paren {\neg p \land \neg q}$

Proof:
{{BeginTableau|p \lor q \vdash \neg \paren {\neg p \land \neg q} }}
{{Premise|1|p \lor q}}
{{Assumption|2|\neg p \land \neg q}}
{{Simplification|3|2|\neg p|2|1}}
{{Simplification|4|2|\neg q|2|2}}
{{Assumption|5|p}}
{{NonContradiction|6|2, 5|5|3}}
{{Assumption|7|q}}
{{NonContradiction|8|2, 7|7|4}}
{{ProofByCases|9|1, 2|\bot|1|5|6|7|8}}
{{Contradiction|10|1|\neg \paren {\neg p \land \neg q}|2|9}}
{{EndTableau|qed}}
Theorem: De Morgan's Laws (Logic)/Disjunction/Formulation 1/Reverse Implication

:$\neg \paren {\neg p \land \neg q} \vdash p \lor q$

Proof:
{{BeginTableau|\neg \paren {\neg p \land \neg q} \vdash p \lor q}}
{{Premise|1|\neg \paren {\neg p \land \neg q} }}
{{Assumption|2|\neg \paren {p \lor q} }}
{{DeMorgan|3|2|\neg p \land \neg q|2|Conjunction of Negations}}
{{NonContradiction|4|1, 2|3|1}}
{{Reductio|5|1|p \lor q|2|4}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum}}
Theorem: De Morgan's Laws (Logic)/Disjunction/Formulation 1

:$p \lor q \dashv \vdash \neg \paren {\neg p \land \neg q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccc||cccccc|} \hline
p & \lor & q & \neg & (\neg & p & \land & \neg & q) \\
\hline
\F & \F & \F & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \F & \T & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Requirement for Connected Domain to be Simply Connected Domain

Then $D$ is '''simply connected''' {{iff}} all paths in $D$ with the same initial points and end points are path-homotopic.
That is, given two paths in $D$:
:$\gamma: \closedint a b \to D$
:$\sigma: \closedint c d \to D$
with $\map \gamma a = \map \sigma c$ and $\map \gamma b = \map \sigma d$, there exists a continuous function $H: \closedint 0 1 \times \closedint 0 1 \to D$ such that:
:$\map H {s, 0} = \map \gamma s$ for all $s \in \closedint 0 1$
:$\map H {s, 1} = \map \sigma s$ for all $s \in \closedint 0 1$
:$\map H {t, 0} = \map \gamma t$ for all $t \in \closedint 0 1$
:$\map H {t, 1} = \map \sigma t$ for all $t \in \closedint 0 1$

Proof:
From Open Domain is Connected iff it is Path-Connected, it follows that $D$ is path-connected.
The results now follows by the definition of simply connected sets.
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction

=== Disjunction is Left Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive}}
=== Disjunction is Right Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
p & \lor & (q & \land & r) & (p & \lor & q) & \land & (p & \lor & r) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \F & \F & \T & \T & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \F & \F & \T & \T & \F & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \F & \T & \T & \T & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction

=== Disjunction is Left Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive}}
=== Disjunction is Right Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive}}

Proof:
{{BeginTableau|\vdash \paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} } }}
{{Assumption|1|p \lor \paren {q \land r} }}
{{SequentIntro|2|1|\paren {p \lor q} \land \paren {p \lor r}|1|Disjunction is Left Distributive over Conjunction: Formulation 1}}
{{Implication|3||\paren {p \lor \paren {q \land r} } \implies \paren {\paren {p \lor q} \land \paren {p \lor r} }|1|2}}
{{Assumption|4|\paren {p \lor q} \land \paren {p \lor r} }}
{{SequentIntro|5|4|p \lor \paren {q \land r}|4|Disjunction is Left Distributive over Conjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \lor q} \land \paren {p \lor r} } \implies \paren {p \lor \paren {q \land r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction

=== Disjunction is Left Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive}}
=== Disjunction is Right Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|} \hline
p & \lor & (q & \land & r) & \iff & (p & \lor & q) & \land & (p & \lor & r) \\
\hline
\F & \F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \T & \F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \F & \T & \F & \T & \T & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \F & \F & \T & \T & \T & \F & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \F & \T & \T & \T & \T & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Disjunction Distributes over Conjunction

=== Disjunction is Left Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive}}
=== Disjunction is Right Distributive over Conjunction ===
{{:Rule of Distribution/Disjunction Distributes over Conjunction/Right Distributive}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
(q & \land & r) & \lor & p & (q & \lor & p) & \land & (r & \lor & p) \\
\hline
F & F & F & F & F & F & F & F & F & F & F & F \\
F & F & F & T & T & F & T & T & T & F & T & T \\
F & F & T & F & F & F & F & F & F & T & T & F \\
F & F & T & T & T & F & T & T & T & T & T & T \\
T & F & F & F & F & T & T & F & F & F & F & F \\
T & F & F & T & T & T & T & T & T & F & T & T \\
T & T & T & T & F & T & T & F & T & T & T & F \\
T & T & T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction

=== Conjunction is Left Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive}}
=== Conjunction is Right Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
p & \land & (q & \lor & r) & (p & \land & q) & \lor & (p & \land & r) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \T & \T & \F & \F & \F & \F & \F & \F & \T \\
\F & \F & \T & \T & \F & \F & \F & \T & \F & \F & \F & \F \\
\F & \F & \T & \T & \T & \F & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction

=== Conjunction is Left Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive}}
=== Conjunction is Right Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive}}

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} } }}
{{Assumption|1|p \land \paren {q \lor r} }}
{{SequentIntro|2|1|\paren {\paren {p \land q} \lor \paren {p \land r} }|1|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }|1|2}}
{{Assumption|4|\paren {p \land q} \lor \paren {p \land r} }}
{{SequentIntro|5|4|p \land \paren {q \lor r}|4|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction

=== Conjunction is Left Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive}}
=== Conjunction is Right Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive}}

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} } }}
{{TheoremIntro|1|\paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }|Conjunction Distributes over Disjunction: Forward Implication}}
{{TheoremIntro|2|\paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }|Conjunction Distributes over Disjunction: Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction

=== Conjunction is Left Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive}}
=== Conjunction is Right Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|} \hline
p & \land & (q & \lor & r) & \iff & (p & \land & q) & \lor & (p & \land & r) \\
\hline
\F & \F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \T & \T & \T & \F & \F & \F & \F & \F & \F & \T \\
\F & \F & \T & \T & \F & \T & \F & \F & \T & \F & \F & \F & \F \\
\F & \F & \T & \T & \T & \T & \F & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction

=== Conjunction is Left Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive}}
=== Conjunction is Right Distributive over Disjunction ===
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc||ccccccc|} \hline
(q & \lor & r) & \land & p & (q & \land & p) & \lor & (r & \land & p) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F & \F & \T & \F & \F & \F & \T \\
\F & \T & \T & \F & \F & \F & \F & \F & \F & \T & \F & \F \\
\F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T & \T \\
\T & \T & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \T & \T & \F & \F & \T \\
\T & \T & \T & \F & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2

:$\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }$

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} } }}
{{Assumption|1|p \land \paren {q \lor r} }}
{{SequentIntro|2|1|\paren {\paren {p \land q} \lor \paren {p \land r} }|1|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }|1|2}}
{{Assumption|4|\paren {p \land q} \lor \paren {p \land r} }}
{{SequentIntro|5|4|p \land \paren {q \lor r}|4|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2

:$\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }$

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} } }}
{{TheoremIntro|1|\paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }|Conjunction Distributes over Disjunction: Forward Implication}}
{{TheoremIntro|2|\paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }|Conjunction Distributes over Disjunction: Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2

:$\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|} \hline
p & \land & (q & \lor & r) & \iff & (p & \land & q) & \lor & (p & \land & r) \\
\hline
\F & \F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \T & \T & \T & \F & \F & \F & \F & \F & \F & \T \\
\F & \F & \T & \T & \F & \T & \F & \F & \T & \F & \F & \F & \F \\
\F & \F & \T & \T & \T & \T & \F & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
p & \land & (q & \lor & r) & (p & \land & q) & \lor & (p & \land & r) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \T & \T & \F & \F & \F & \F & \F & \F & \T \\
\F & \F & \T & \T & \F & \F & \F & \T & \F & \F & \F & \F \\
\F & \F & \T & \T & \T & \F & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} } }}
{{Assumption|1|p \land \paren {q \lor r} }}
{{SequentIntro|2|1|\paren {\paren {p \land q} \lor \paren {p \land r} }|1|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }|1|2}}
{{Assumption|4|\paren {p \land q} \lor \paren {p \land r} }}
{{SequentIntro|5|4|p \land \paren {q \lor r}|4|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|6||\paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} } }}
{{TheoremIntro|1|\paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }|Conjunction Distributes over Disjunction: Forward Implication}}
{{TheoremIntro|2|\paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }|Conjunction Distributes over Disjunction: Reverse Implication}}
{{BiconditionalIntro|3||\paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|} \hline
p & \land & (q & \lor & r) & \iff & (p & \land & q) & \lor & (p & \land & r) \\
\hline
\F & \F & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \T & \T & \T & \F & \F & \F & \F & \F & \F & \T \\
\F & \F & \T & \T & \F & \T & \F & \F & \T & \F & \F & \F & \F \\
\F & \F & \T & \T & \T & \T & \F & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive

==== Formulation 1 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Distribution/Conjunction Distributes over Disjunction/Right Distributive/Formulation 2}}

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc||ccccccc|} \hline
(q & \lor & r) & \land & p & (q & \land & p) & \lor & (r & \land & p) \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \F & \F & \F & \T & \F & \F & \T & \F & \F & \F & \T \\
\F & \T & \T & \F & \F & \F & \F & \F & \F & \T & \F & \F \\
\F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T & \T \\
\T & \T & \F & \F & \F & \T & \F & \F & \F & \F & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \T & \T & \F & \F & \T \\
\T & \T & \T & \F & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}