avewright/proofwiki-math huggingface dataset:
Theorem: Rule of Exportation/Formulation 2

:$\vdash \paren {\paren {p \land q} \implies r} \iff \paren {p \implies \paren {q \implies 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 are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|ccccc|} \hline
(p & \implies & (q & \implies & r)) & \implies & ((p & \land & q) & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \T & \F & \T & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \F & \T & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \F & \T & \T & \T \\
\T & \T & \F & \T & \F & \T & \T & \F & \F & \T & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Exportation/Formulation 2/Forward Implication

:$\vdash \paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption|1|\paren {p \land q} \implies r}}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{Conjunction|4|2, 3|p \land q|2|3}}
{{ModusPonens|5|1, 2, 3|r|1|4}}
{{Implication|6|1, 2|q \implies r|3|5}}
{{Implication|7|1|p \implies \paren {q \implies r} |2|6}}
{{Implication|8||\paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} }|1|7}}
{{EndTableau|lemma}}
Theorem: Rule of Exportation/Formulation 2/Forward Implication

:$\vdash \paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption|1|\paren {p \land q} \implies r}}
{{SequentIntro|2|1|p \implies \paren {q \implies r}|1|Rule of Exportation: Formulation 1: Forward Implication}}
{{Implication|3||\paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Exportation/Formulation 2/Forward Implication

:$\vdash \paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies 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 are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|ccccc|} \hline
((p & \land & q) & \implies & r) & \implies & (p & \implies & (q & \implies & r)) \\
\hline
\F & \F & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \F & \F & \T & \T & \T & \F & \T & \F & \T & \T \\
\F & \F & \T & \T & \F & \T & \F & \T & \T & \F & \F \\
\F & \F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \T & \T & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \T & \F & \F & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Exportation/Formulation 2/Reverse Implication

:$\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r} }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{Assumption|2|p \land q}}
{{Simplification|3|2|p|2|1}}
{{Simplification|4|2|q|2|2}}
{{ModusPonens|5|1, 2|q \implies r|1|3}}
{{ModusPonens|6|1, 2|r|5|4}}
{{Implication|7|1|\paren {p \land q} \implies r|2|6}}
{{Implication|8||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}|1|7}}
{{EndTableau|lemma}}
Theorem: Rule of Exportation/Formulation 2/Reverse Implication

:$\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}$

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r} }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{SequentIntro|2|1|\paren {p \land q} \implies r|1|Rule of Exportation: Formulation 1: Reverse Implication}}
{{Implication|3||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}|1|2}}
{{EndTableau|qed}}
Theorem: Rule of Exportation/Formulation 2/Reverse Implication

:$\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies 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 are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|ccccc|} \hline
(p & \implies & (q & \implies & r)) & \implies & ((p & \land & q) & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \T & \F & \T & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \F & \T & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \F & \T & \T & \T \\
\T & \T & \F & \T & \F & \T & \T & \F & \F & \T & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Exportation/Formulation 1/Forward Implication

:$\paren {p \land q} \implies r \vdash p \implies \paren {q \implies r}$

Proof:
{{BeginTableau|\paren {p \land q} \implies r \vdash p \implies \paren {q \implies r} }}
{{Premise|1|\paren {p \land q} \implies r}}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{Conjunction|4|2, 3|p \land q|2|3}}
{{ModusPonens|5|1, 2, 3|r|1|4}}
{{Implication|6|1, 2|q \implies r|3|5}}
{{Implication|7|1|p \implies \paren {q \implies r} |2|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Exportation/Formulation 1/Reverse Implication

:$p \implies \paren {q \implies r} \vdash \paren {p \land q} \implies r$

Proof:
{{BeginTableau|p \implies \paren {q \implies r} \vdash \paren {p \land q} \implies r}}
{{Premise|1|p \implies \paren {q \implies r} }}
{{Assumption|2|p \land q}}
{{Simplification|3|2|p|2|1}}
{{Simplification|4|2|q|2|2}}
{{ModusPonens|5|1, 2|q \implies r|1|3}}
{{ModusPonens|6|1, 2|r|5|4}}
{{Implication|7|1|\paren {p \land q} \implies r|2|6}}
{{EndTableau|qed}}
Theorem: Rule of Commutation/Conjunction/Formulation 1

:$p \land q \dashv \vdash q \land p$

Proof:
{{BeginTableau|p \land q \vdash q \land p}}
{{Premise|1|p \land q}}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|q|1|2}}
{{Conjunction|4|1|q \land p|3|2}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|q \land p \vdash p \land q}}
{{Premise|1|q \land p}}
{{Simplification|2|1|q|1|1}}
{{Simplification|3|1|p|1|2}}
{{Conjunction|4|1|p \land q|3|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Commutation/Conjunction/Formulation 1

:$p \land q \dashv \vdash q \land p$

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||ccc|} \hline
p & \land & q & q & \land & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \F & \T & \T & \F & \F \\
\T & \F & \F & \F & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Commutation/Disjunction/Formulation 1

:$p \lor q \dashv \vdash q \lor p$

Proof:
{{BeginTableau|p \lor q \vdash q \lor p}}
{{Premise|1|p \lor q}}
{{Assumption|2|p}}
{{Addition|3|2|q \lor p|2|2}}
{{Assumption|4|p}}
{{Addition|5|4|q \lor p|4|1}}
{{ProofByCases|6|1|q \lor p|1|2|3|4|5}}
{{EndTableau}}
{{qed}}
{{BeginTableau|q \lor p \vdash p \lor q}}
{{Premise|1|q \lor p}}
{{Assumption|2|q}}
{{Addition|3|2|p \lor q|2|2}}
{{Assumption|4|p}}
{{Addition|5|4|p \lor q|4|1}}
{{ProofByCases|6|1|p \lor q|1|2|3|4|5}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Commutation/Disjunction/Formulation 1

:$p \lor q \dashv \vdash q \lor p$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, in both cases, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc||ccc|} \hline
p & \lor & q & q & \lor & p \\
\hline
\F & \F & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Commutation/Conjunction/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \land q} \iff \paren {q \land p} }}
{{Assumption |1|p \land q}}
{{Commutation|2|1|q \land p|1|Conjunction}}
{{Implication|3||\paren {p \land q} \implies \paren {q \land p}|1|2}}
{{Assumption |4|q \land p}}
{{Commutation|5|4|p \land q|4|Conjunction}}
{{Implication|6||\paren {q \land p} \implies \paren {p \land q}|4|5}}
{{BiconditionalIntro|7||\paren {p \land q} \iff \paren {q \land p}|3|6}}
{{EndTableau|qed}}
Theorem: Rule of Commutation/Disjunction/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \lor q} \iff \paren {q \lor p} }}
{{Assumption|1|p \lor q}}
{{Commutation|2|1|q \lor p|1|Disjunction}}
{{Implication|3||\paren {p \lor q} \implies \paren {q \lor p}|1|2}}
{{Assumption|4|q \lor p}}
{{Commutation|5|4|p \lor q|4|Disjunction}}
{{Implication|6||\paren {q \lor p} \implies \paren {p \lor q}|4|5}}
{{BiconditionalIntro|7||\paren {p \lor q} \iff \paren {q \lor p}|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Commutation/Disjunction/Formulation 2

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc|c|ccc|} \hline
(p & \lor & q) & \iff & (q & \lor & p) \\
\hline
\F & \F & \F & \T & \F & \F & \F \\
\F & \T & \T & \T & \T & \T & \F \\
\T & \T & \F & \T & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Combination Theorem for Complex Derivatives/Product Rule

:$\map {\paren {f g}'} z = \map {f'} z \map g z + \map f z \map {g'} z$

Proof:
Define $k: D \to \C$ as the pointwise product of $f$ and $g$, so $k = fg$.
Let $z_0 \in D$ be a point in $D$.
{{begin-eqn}}
{{eqn | l = \map {k'} {z_0}
      | r = \lim_{h \mathop \to 0} \frac {\map k {z_0 + h} - \map k {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} \, \map g {z_0 + h} - \map f {z_0} \, \map g {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} \, \map g {z_0 + h} - \map f {z_0 + h} \, \map g {z_0} + \map f {z_0 + h} \, \map g {z_0} - \map f {z_0} \, \map g {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\map f {z_0 + h} \frac {\map g {z_0 + h} - \map g {z_0} } h + \frac {\map f {z_0 + h} - \map f {z_0} } h \, \map g {z_0} }
      | c =
}}
{{eqn | r = \map f {z_0} \, \map {g'} {z_0} + \map {f'} {z_0} \, \map g {z_0}
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall z \in D
      | l = \map {k'} z
      | r = \map f z \, \map {g'} z + \map {f'} z \, \map g z
      | c = {{Defof|Derivative of Complex Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Combination Theorem for Complex Derivatives/Product Rule

:$\map {\paren {f g}'} z = \map {f'} z \map g z + \map f z \map {g'} z$

Proof:
Denote the open ball of $0$ by radius $r \in \R_{>0}$ as $\map {B_r} 0$.
Let $z \in D$.
By the Epsilon-Function Complex Differentiability Condition, it follows that there exists $r \in \R_{>0}$ such that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + \map h {\map {f'} z + \map {\epsilon_f} h}$
:$\map g {z + h} = \map g z + \map h {\map {g'} z + \map {\epsilon_g} h}$
where $\epsilon_f, \epsilon_g: \map {B_r} 0 \setminus \set 0 \to \C$ are complex functions that converge to $0$ as $h$ tends to $0$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f g} } {z + h}
      | r = \map f z \map g z + \map h {\map f z \map {g'} z + \map f z \map {\epsilon_g} h} + h \paren {\map g z \map {f'} z + \map g z \map {\epsilon_f} h} + {h^2} \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h}
}}
{{eqn | r = \map {\paren {f g} } z + h \paren {\map {f'} z \map g z + \map f z \map {g'} z + h \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h} }
}}
{{end-eqn}}
Define $\epsilon: \map {B_r} 0 \setminus \set 0 \to \C$ by:
:$\map \epsilon h = h \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h}$
From Product Rule for Limits of Complex Functions and Combined Sum Rule for Limits of Complex Functions:
:$\ds \lim_{h \mathop \to 0} \map \epsilon h = \paren {\lim_{h \mathop \to 0} h} \paren {\lim_{h \mathop \to 0} \paren {\map {f'} z + \map {\epsilon_f} h} } \paren {\lim_{h \mathop \to 0} \paren {\map {g'} z + \map {\epsilon_g} h} } = 0$
Then the Epsilon-Function Complex Differentiability Condition shows that:
:$\map {\paren {f g}'} z = \map {f'} z \map g z + \map f z \map {g'} z$
{{qed}}
Theorem: Dedekind Completion is Unique up to Isomorphism

Let $S$ be an ordered set.
Let $\struct {X, f}$ and $\struct {Y, g}$ be Dedekind completions of $S$.
Then there exists a unique order isomorphism $\phi: X \to Y$ such that $\phi \circ f = g$.

Proof:
By assumption, $\struct {X, f}$ is a Dedekind completion of $S$.
Also, $g: S \to Y$ is an order embedding and $Y$ is Dedekind complete.
Hence by definition of Dedekind completion, there exists a unique $\phi: X \to Y$ such that:
:$\phi \circ f = g$
It only remains to show that $\psi$ is an order isomorphism.
By reversing the roles of $X$ and $Y$ in the above, we obtain a unique $\psi: Y \to X$ subject to:
:$\psi \circ g = f$
Therefore:
:$\psi \circ \phi \circ f = f$
:$\phi \circ \psi \circ g = g$
By the uniqueness clause of the definition of Dedekind completion, it follows that:
:$\psi \circ \phi = I_X$
:$\phi \circ \psi = I_Y$
where $I_X$ and $I_Y$ are the identity mappings on $X$ and $Y$ respectively.
Hence $\psi$ is an order isomorphism.
{{qed}}
Theorem: Combination Theorem for Complex Derivatives/Combined Sum Rule

Let $\map {\dfrac \d {\d z} } {c f + w g}$ denote the derivative of $c f + w g$.
Then:
:$\map {\map {\dfrac \d {\d z} } {c f + w g} } z = c \dfrac \d {\d z} \map f z + w \dfrac \d {\d z} \map g z$

Proof:
{{begin-eqn}}
{{eqn | l = c \dfrac \d {\d z} \map f z + w \dfrac \d {\d z} \map g z
      | r = \map {\map {\dfrac \d {\d z} } {c f} } z + \map {\map {\dfrac \d {\d z} } {w g} } z
      | c = Combination Theorem for Complex-Differentiable Functions: Multiple Rule
}}
{{eqn | r = \map {\map {\dfrac \d {\d z} } {c f + w g} } z
      | c = Combination Theorem for Complex-Differentiable Functions:Sum Rule
}}
{{end-eqn}}
{{qed}}
Theorem: Existence of Dedekind Completion

Let $\struct {S, \preceq}$ be an ordered set.
Then there exists a Dedekind completion of $S$.
That is, there exists a Dedekind complete ordered set $\tilde S$ and an order embedding $\phi: S \to \tilde S$ such that:
:For all Dedekind complete ordered sets $X$, and for all order embeddings $f: S \to X$, there exists an order embedding $\tilde f: \tilde S \to X$ such that:
::$\tilde f \circ \phi = f$

Proof:
For all subsets $I \subseteq S$, define:
:$\map {\operatorname U} I = \left\{{x \in S: x}\right.$ is an upper bound for $\left.{I}\right\}$
:$\map {\operatorname L} I = \left\{{x \in S: x}\right.$ is a lower bound for $\left.{I}\right\}$
Note that, for all $I, J \subseteq S$:
:$I \subseteq \map {\operatorname {LU} } I$
:$I \subseteq J \implies \map {\operatorname {LU} } I \subseteq \map {\operatorname {LU} } J$
:$\map {\operatorname {ULU} } I = \map {\operatorname U} I$
All of the above follow directly from the relevant definitions.
Let:
:$\tilde S = \left\{{I \subseteq S: I = \map {\operatorname {LU} } I}\right.$, $I$ is non-empty and bounded above$\left.{}\right\}$
We have that $\struct {\tilde S, \subseteq}$ is an ordered set.
Let $A \subseteq \tilde S$ be non-empty and bounded above.
By Union is Smallest Superset: General Result, $\ds \bigcup A$ is non-empty and bounded above.
It follows that:
:$\ds {\operatorname{LU} } {\bigcup A} \in \tilde S$
From Set is Subset of Union: General Result, it follows that $\ds \map {\operatorname{LU} } {\bigcup A}$ is an upper bound for $A$.
If $I \in \tilde S$ is an upper bound for $A$, then, by Union is Smallest Superset: General Result:
:$\ds \bigcup A \subseteq I$
It follows that:
:$\ds \map {\operatorname{LU} } {\bigcup A} \subseteq \map {\operatorname{LU} } I = I$
Hence:
:$\ds \operatorname{LU} {\bigcup A} = \sup A$
By definition, $\struct {\tilde S, \subseteq}$ is Dedekind complete.
Let $\phi: S \to \tilde S$ be the order embedding defined as:
:$\forall x \in S: \map \phi x = x^\preceq$
where $x^\preceq$ denotes the weak lower closure of $x$ (in $S$).
Let $\struct {X, \preccurlyeq}$ be a Dedekind complete ordered set, and let $f: S \to X$ be an order embedding.
Let $\tilde f: \tilde S \to X$ be the increasing mapping defined as:
:$\forall I \in \tilde S: \map {\tilde f} I = \sup \map f I$
where $\map f I$ denotes the image of $I$ under $f$.
Then $\tilde f \circ \phi = f$.
Let $I, J \in \tilde S$ such that $\map {\tilde f} I \preccurlyeq \map {\tilde f} J$.
Then $\forall x \in I: \forall u \in \map {\operatorname U} J: \map f x \preccurlyeq \map {\tilde f} J \preccurlyeq \map f u$.
Since $f$ is an order embedding, it follows that $I \subseteq \map {\operatorname {LU} } J = J$.
Hence, $\tilde f$ is an order embedding.
{{qed}}
Theorem: Reflexive Reduction of Transitive Antisymmetric Relation is Strict Ordering

Let $S$ be a set.
Let $\RR$ be a transitive, antisymmetric relation on $S$.
Let $\RR^\ne$ denote the reflexive reduction of $\RR$.
Then $\RR^\ne$ is a strict ordering.

Proof:
To show that $\RR^\ne$ is a strict ordering, it is sufficient to show that $\RR^\ne$ is antireflexive and transitive.
Theorem: Reflexive Reduction of Antisymmetric Relation is Asymmetric

Let $S$ be a set.
Let $\RR$ be an antisymmetric relation on $S$.
Let $\RR^\ne$ be the reflexive reduction of $\RR$.
Then $\RR^\ne$ is asymmetric.

Proof:
{{AimForCont}} $\RR^\ne$ is not asymmetric.
That is:
:$\exists a, b \in S: a \mathrel {\RR^\ne} b$ and $b \mathrel {\RR^\ne} a$
Then by the definition of reflexive reduction:
:$a \mathrel \RR b$, $b \mathrel \RR a$
and $a \ne b$.
But this contradicts the antisymmetry of $\RR$.
Thus, by definition, $\RR^\ne$ is an asymmetric relation.
{{qed}}
Theorem: Reductio ad Absurdum/Variant 1

:$\neg p \implies \bot \vdash p$

Proof:
{{BeginTableau|\neg p \implies \bot \vdash p}}
{{Premise|1|\neg p \implies \bot}}
{{Assumption|2|\neg p}}
{{ModusPonens|3|1, 2|\bot|1|2}}
{{Contradiction|4|1|\neg \neg p|2|3}}
{{DoubleNegElimination|5|1|p|4}}
{{EndTableau|qed}}
Theorem: Reductio ad Absurdum/Variant 1

:$\neg p \implies \bot \vdash p$

Proof:
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|cccc||c|} \hline
\neg & p & \implies & \bot & p \\
\hline
\T & \F & \F & \F & \F \\
\F & \T & \T & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Reductio ad Absurdum/Variant 2

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

Proof:
{{BeginTableau|\neg p \implies \left({q \land \neg q}\right) \vdash p}}
{{Premise|1|\neg p \implies \left({q \land \neg q}\right)}}
{{Assumption|2|\neg p}}
{{ModusPonens|3|1, 2|q \land \neg q|1|2}}
{{Simplification|4|1, 2|q|3|1}}
{{Simplification|5|1, 2|\neg q|3|2}}
{{NonContradiction|6|1, 2|4|5}}
{{Contradiction|7|1|\neg \neg p|2|6}}
{{DoubleNegElimination|8|1|p|7}}
{{EndTableau}}
{{qed}}
Theorem: Reductio ad Absurdum/Variant 2

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

Proof:
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccccc||c|} \hline
\neg & p & \implies & (q & \land & \neg & q) & p \\
\hline
\T & \F & \F & \F & \F & \T & \F & \F \\
\T & \F & \F & \T & \F & \F & \T & \F \\
\F & \T & \T & \F & \F & \T & \F & \T \\
\F & \T & \T & \T & \F & \F & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Proof by Contradiction/Variant 1

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

Proof:
{{BeginTableau|\paren {p \vdash \paren {q \land \neg q} } \vdash \neg p}}
{{Premise|1|p \vdash \paren {q \land \neg q} }}
{{Assumption|2|p}}
{{SequentIntro|3|1, 2|q \land \neg q|1, 2|{{hypothesis}} }}
{{Simplification|4|1, 2|q|3|1}}
{{Simplification|5|1, 2|\neg q|3|2}}
{{NonContradiction|6|1, 2|4|5}}
{{Contradiction|7|1|\neg p|2|6}}
{{EndTableau|qed}}
Theorem: Equivalence of Definitions of Topological Group

Let $\struct {G, \odot}$ be a group.
On its underlying set $G$, let $\struct {G, \tau}$ be a topological space.
{{TFAE|def = Topological Group}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\struct {G, \odot, \tau}$ be a topological group by Definition 1.
Let $\phi: \struct {G, \tau} \to \struct {G, \tau}$ be the mapping defined as:
:$\forall x \in G: \map \phi x = x^{-1}$
By definition:
:$\odot: \struct {G, \tau} \times \struct {G, \tau} \to \struct {G, \tau}$ is a continuous mapping
:$\phi: \struct {G, \tau} \to \struct {G, \tau}$ is a continuous mapping
Let $\phi': G \times G \to G \times G$ be defined by:
:$\map {\phi'} {x, y} = \tuple {x, \map \phi y}$
Let $\phi_1: G \times G \to G$ be defined as:
:$\map {\phi_1} {x, y} = x$
Let $\phi_2: G \times G \to G$ be defined as:
:$\map {\phi_2} {x, y} = y^{-1}$
Then for arbitrary open set $V \subset G$, both sets
:$\phi_1^{-1} \sqbrk V = V \times G$
and
:$\phi_2^{-1} \sqbrk V = G \times \phi^{-1} \sqbrk V$
are open in $G \times G$, thus $\phi_1$ and $\phi_2$ are continuous.
Because:
:$\map {\phi'} {x, y} = \tuple {\map {\phi_1} x, \map {\phi_2} y}$
by Continuous Mapping to Product Space, $\phi'$ is continuous.
Let the mapping $\psi: \struct {G, \tau} \times \struct {G, \tau} \to \struct {G, \tau}$ be defined as:
:$\psi = \odot \circ \phi'$
where $\circ$ denotes composition of mappings.
By Composite of Continuous Mappings is Continuous, $\psi$ is continuous.
Then:
{{begin-eqn}}
{{eqn | l = \map \psi {x, y}
      | r = \map {\paren {\odot \circ \phi'} } {x, y}
      | c = Definition of $\psi$
}}
{{eqn | r = \map \odot {\map {\phi'} {x, y} }
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map \odot {x, \map \phi y}
      | c = Definition of $\phi'$
}}
{{eqn | r = \map \odot {x, y^{-1} }
      | c = Definition of $\phi$
}}
{{eqn | r = x \odot y^{-1}
      | c = Definition of $\odot$
}}
{{end-eqn}}
demonstrating that:
:$\map \psi {x, y} = x \odot y^{-1}$
Thus $\struct {G, \odot, \tau}$ is a topological group by Definition 2.
{{qed|lemma}}
Theorem: Conditional is Left Distributive over Conjunction/Formulation 1/Forward Implication

:$p \implies \paren {q \land r} \vdash \paren {p \implies q} \land \paren {p \implies r}$

Proof:
{{BeginTableau|p \implies \paren {q \land r} \vdash \paren {p \implies q} \land \paren {p \implies r} }}
{{Premise|1|p \implies \paren {q \land r} }}
{{Assumption|2|p}}
{{ModusPonens|3|1, 2|q \land r|1|2}}
{{Simplification|4|1, 2|q|3|1}}
{{Simplification|5|1, 2|r|3|2}}
{{Implication|6|1|p \implies q|2|4}}
{{Implication|7|1|p \implies r|2|5}}
{{Conjunction|8|1|\paren {p \implies q} \land \paren {p \implies r}|6|7}}
{{EndTableau|qed}}
Theorem: Conditional is Left Distributive over Conjunction/Formulation 1/Reverse Implication

:$\paren {p \implies q} \land \paren {p \implies r} \vdash p \implies \paren {q \land r}$

Proof:
{{BeginTableau|\paren {p \implies q} \land \paren {p \implies r} \vdash p \implies \paren {q \land r} }}
{{Premise|1|\paren {p \implies q} \land \paren {p \implies r} }}
{{SequentIntro|2|1|\paren {p \land p} \implies \paren {q \land r}|1|Praeclarum Theorema}}
{{Assumption|3|p}}
{{Idempotence|4|3|p \land p|3|Conjunction}}
{{ModusPonens|5|1, 3|q \land r|2|4}}
{{Implication|6|1|p \implies \paren {q \land r}|3|5}}
{{EndTableau}}
{{qed}}