% -*- TeX:EN -*-
%%% ====================================================================
%%% @LaTeX-file    qedeq_formal_logic_v1
%%% Generated from http://www.qedeq.org/0_04_05/doc/math/qedeq_formal_logic_v1.xml
%%% Generated at   2013-02-05 00:28:45.471
%%% ====================================================================

%%% Permission is granted to copy, distribute and/or modify this document
%%% under the terms of the GNU Free Documentation License, Version 1.2
%%% or any later version published by the Free Software Foundation;
%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.

\documentclass[a4paper,german,10pt,twoside]{book}
\usepackage[english]{babel}
\usepackage{makeidx}
\usepackage{amsmath,amsthm,amssymb}
\usepackage{color}
\usepackage{xr}
\usepackage{tabularx}
\usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen,
   unicode=true,colorlinks=true,linkcolor=webgreen,
   pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref}
\definecolor{webgreen}{rgb}{0,.5,0}
\usepackage{epsfig,longtable}
\usepackage{graphicx}
\usepackage[all]{hypcap}

\newtheorem{thm}{Theorem}
\newtheorem{cor}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{ax}{Axiom}
\newtheorem{rul}{Rule}

\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{idefn}[defn]{Initial Definition}

\theoremstyle{remark}
\newtheorem{rem}[thm]{Remark}
\newtheorem*{notation}{Notation}


\addtolength{\textheight}{7\baselineskip}
\addtolength{\topmargin}{-5\baselineskip}

\setlength{\parindent}{0pt}

\frenchspacing \sloppy

\makeindex


\title{Formal Predicate Calculus}
\author{
Michael Meyling
}

\begin{document}

\maketitle

\setlength{\parskip}{5pt plus 2pt minus 1pt}
\mbox{}
\vfill

\par
The source for this document can be found here:
\par
\url{http://www.qedeq.org/0_04_05/doc/math/qedeq_formal_logic_v1.xml}

\par
Copyright by the authors. All rights reserved.
\par
If you have any questions, suggestions or want to add something to the list of modules that use this one, please send an email to the address \href{mailto:mime@qedeq.org}{mime@qedeq.org}

\par
The authors of this document are:
Michael Meyling \href{mailto:michael@meyling.com}{michael@meyling.com}

\setlength{\parskip}{0pt}
\tableofcontents

\setlength{\parskip}{5pt plus 2pt minus 1pt}

\chapter*{Summary\index{summary}} \label{chapter1} \hypertarget{chapter1}{}
\addcontentsline{toc}{chapter}{Summary\index{summary}}

In this text we present the development of predicate calculus in axiomatic form.
The language of our calculus bases on the formalizations of \emph{D.~Hilbert}, \emph{W.~Ackermann}\cite{hilback}, \emph{P.~S.~Novikov}\cite{novikov}, \emph{V.~Detlovs} and \emph{K.~Podnieks}\cite{detnieks}. New rules can be derived from the herein presented logical axioms and basic inference rules. Only these meta rules lead to a smooth flowing logical argumentation.
For background informations see under \url{http://www.ltn.lv/~podnieks/mlog/ml.htm}
and \url{http://en.wikipedia.org/wiki/Propositional_calculus}.

%% end of chapter Summary\index{summary}

\chapter{Language} \label{chapter2} \hypertarget{chapter2}{}

In this chapter we define a formal language to express mathematical propositions in a very precise way. Although this document describes a very formal approach to express mathematical content it is not sufficent to serve as a definition for an computer readable document format. Therefore such an extensive specification has to be done elsewhere. The choosen format is the \emph{Extensible Markup Language} abbreviated \emph{XML}. XML is a set of rules for encoding documents electronically.\footnote{See \url{http://www.w3.org/XML/} for more information.}
The according formal syntax specification can be found at \url{http://www.qedeq.org/current/xml/qedeq.xsd}.
It specifies a complete mathematical document format that enables the generation of \LaTeX books and makes automatic proof checking possible. 
Further syntax restrictions and some explanations can be found at \url{http://www.qedeq.org/current/doc/project/qedeq_logic_language_en.pdf}.
%%% TODO explain XSD, XML etc.

\par          
Even this document is (or was generated) from an XML file that can be found here: \url{http://wwww.qedeq.org/0_04_05/doc/math/qedeq_logic_v1.xml}.
But now we just follow the traditional mathematical way to present the elements of mathematical logic.

\section{Terms\index{term} and Formulas\index{formula}} \label{chapter2_section1} \hypertarget{chapter2_section1}{}
We use the \emph{logical symbols} 
$L = \{$ \mbox{`$\neg$'}, \mbox{`$\vee$'}, \mbox{`$\wedge$'}, \mbox{`$\leftrightarrow$'}, \mbox{`$\rightarrow$'}, \mbox{`$\forall$'}, \mbox{`$\exists$'} $\}$, the \emph{predicate constants}\index{predicate constant}\index{constant!predicate} $C = \{c^k_i~|~i, k \in \omega\}$, the \emph{function variables}\index{function variable}\index{variable!function}\footnote{Function variables are used for a shorter notation. For example writing an identity proposition $x = y \rightarrow f(x) = f(y)$. Also this introduction prepares for the syntax extension for functional classes.} $F = \{f^k_i~|~i, k \in \omega \land k > 0\}$, the \emph{function constants}\index{function constant}\index{constant!function}\footnote{Function constants are also introduced for convenience and are used for direct defined class functions. For example to define building of the power class operator, the union and intersection operator and the successor function. All these function constants can be interpreted as abbreviations.} $H = \{h^k_i~|~i, k \in \omega\}$, the \emph{subject variables}\index{subject variable}\index{variable!subject} $V = \{v_i~|~i \in \omega\}$, as well as
\emph{predicate variables}\index{predicate variable}\index{variable!predicate} $P = \{p^k_i~|~i, k \in \omega\}$.\footnote{By $\omega$ we understand the natural numbers including zero. All involved symbols are pairwise disjoint. 
Therefore we can conclude for example: $f^k_i = f^{k'}_{i'} \rightarrow (k = k' \land i = i')$ and $h^k_i \neq v_j$.} 
For the \emph{arity}\index{arity} or \emph{rank}\index{rank} of an operator we take the upper index. The set of predicate variables with zero arity is also called set of \emph{proposition variables}\index{proposition variable}\index{variable!proposition} or \emph{sentence letters}\index{sentence letters}: $A := \{p_i^0~|~i \in \omega \}$.
For subject variables we write short hand certain lower letters: \mbox{$v_1 = $ `$u$'}, \mbox{$v_2 = $ `$v$'}, 
\mbox{$v_3 = $ `$w$'}, \mbox{$v_4 = $ `$x$'}, \mbox{$v_5 = $ `$y$'}, \mbox{$v_5 = $ `$z$'}.
Furthermore we use the following short notations: for the predicate variables $p^n_1 = $ `$\phi$' und $p^n_2 = $ `$\psi$', where the appropriate arity $n$ is calculated by counting the subsequent parameters, for the proposition variables
$a_1 = $ `$A$', $a_2 = $ `$B$' and $a_3 = $ `$C$', for the function variables: $f^n_1 = $ `$f$' und $f^n_2 = $ `$g$', where again the appropriate arity $n$ is calculated by counting the subsequent parameters.  All binary propositional operators are written in infix notation. Parentheses surrounding groups of operands and operators are necessary to indicate the 
intended order in which operations are to be performed. E.~g. for the operator $\land$ with the parameters $A$ and $B$ we write $(A \land B)$.


In the absence of parentheses the usual precedence rules determine the order of operations. Especially outermost parentheses are omitted. Also empty parentheses are stripped.

\par
The operators have the order of precedence described below (starting with the highest).
$$
\begin{array}{c}
  \neg, \forall, \exists  \\
  \land \\
  \lor \\
  \rightarrow, \leftrightarrow \\
\end{array}
$$

\par
The term \emph{term\index{term}} is defined recursively as follows:

\begin{enumerate}
\item Every subject variable is a term. 
\item Let $i, k \in \omega$ and let $t_1$, \ldots, $t_k$ be terms. Then $h^k_i(t_1, \ldots, t_k)$ is a term and if $k > 0$, so $f^k_i(t_1, \ldots, t_k)$ is a term too.
\end{enumerate}

Therefore all zero arity function constants $\{h^0_i~|~i \in \omega\}$ are terms. They are called \emph{individual constants}\index{individual constant}\index{constant!individual}.\footnote{In an analogous manner subject variables might be defined as function variables of zero arity. Because subject variables play an important role they have their own notation.}

\par
We define a \emph{formula\index{formula}} and the relations \emph{free}\index{bound subject variable}\index{subject variable!free} and \emph{bound}\index{bound subject variable}\index{subject variable!bound} subject variable recursivly as follows:

\begin{enumerate}

\item Every proposition variable is a formula. Such formulas contain no free or bound subject variables.

\item If $p^k$ is a predicate variable with arity $k$ and $c^k$ is a predicate constant with arity $k$ and $t_1, t_2, \ldots, t_k$ are terms, then $p^k(t_1, t_2, \ldots t_k)$ and $c^k(t_1, t_2, \ldots, t_k)$ are formulas. All subject variables that occur at least in one of $t_1, t_2, \ldots, t_k$ are free subject variables. Bound subject variables does not occur.\footnote{This second item includes the first one, which is only listed for clarity.} 

\item Let $\alpha, \beta$ be formulas in which no subject variables occur bound in one formula and free in the other. Then $\neg \alpha$, $(\alpha \land \beta)$, $(\alpha \lor \beta)$, $(\alpha \rightarrow \beta)$ and $(\alpha \leftrightarrow \beta)$ are also formulas. Subject variables which occur free (respectively bound) in $\alpha$ or $\beta$ stay free (respectively bound).

\item If in the formula $\alpha$ the subject variable $x_1$ occurs not bound\footnote{This means that $x_1$ is free in the formula or does not occur at all.}, then also $\forall x_1~\alpha$ and $\exists x_1~\alpha$ are formulas. The symbol $\forall$ is called \emph{universal quantifier}\index{universal quantifier}\index{quantifier!universal} and $\exists$ as
\emph{existential quantifier}\index{existential quantifier}\index{quantifier!existential}.

Except for $x_1$ all free subject variables of $\alpha$ stay free. All bound subject variables are still bound and additionally $x_1$ is bound too.

\end{enumerate}

All formulas that are only built by usage of 1. and 3. are called formulas of the \emph{propositional calculus}\index{propositional calculus}\index{calculus!propositional}.

\par
For each formula $\alpha$ the following proposition holds: the set of free subject variables is disjoint with the set of bound subject variables..\footnote{Other formalizations allow for example $\forall x_1~\alpha$ also if $x_1$ occurs already bound within $\alpha$. Also propositions like $\alpha(x_1)~\land~(\forall~x_1~\beta)$ are allowed. In this formalizations
free and bound are defined for a single occurrence of a variable.}

\par
If a formula has the form $\forall x_1 ~ \alpha$ respectively $\exists x_1 ~ \alpha$ then the formula $\alpha$ is called the
\emph{scope}\index{scope}\index{quantifier!scope} of the quantifier $\forall$ respectively $\exists$.

\par
All formulas that are used to build up a formula by 1. to 4. are called \emph{part formulas}\index{part formula}\index{formula!part}.


%% end of chapter Language

\chapter{Axioms and Rules of Inference} \label{chapter3} \hypertarget{chapter3}{}

We now state the system of axioms for the propositional calculus and present the rules for obtaining new formulas from them.

\section{Axioms\index{axioms}} \label{chapter3_section1} \hypertarget{chapter3_section1}{}
Here we just list the axioms without further explanations.

\begin{ax}[Implication Introduction\index{implication introduction}]
\label{axiom:THEN-1} \hypertarget{axiom:THEN-1}{}
{\tt \tiny [\verb]axiom:THEN-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (B\ \rightarrow\ A)$
\end{longtable}

\end{ax}


\begin{ax}[Distribute Hypothesis over Implication\index{hypothesis distribution}]
\label{axiom:THEN-2} \hypertarget{axiom:THEN-2}{}
{\tt \tiny [\verb]axiom:THEN-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))$
\end{longtable}

\end{ax}


\begin{ax}[Eliminate Conjunction Right\index{conjunction!elimination}]
\label{axiom:AND-1} \hypertarget{axiom:AND-1}{}
{\tt \tiny [\verb]axiom:AND-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \land\ B)\ \rightarrow\ A$
\end{longtable}

\end{ax}


\begin{ax}[Eliminate Conjunction Left\index{conjunction!elimination}]
\label{axiom:AND-2} \hypertarget{axiom:AND-2}{}
{\tt \tiny [\verb]axiom:AND-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \land\ B)\ \rightarrow\ B$
\end{longtable}

\end{ax}


\begin{ax}[Conjunction Introduction\index{conjunction!introduction}]
\label{axiom:AND-3} \hypertarget{axiom:AND-3}{}
{\tt \tiny [\verb]axiom:AND-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$
\end{longtable}

\end{ax}


\begin{ax}[Disjunction Introduction Right\index{disjunction!introduction}]
\label{axiom:OR-1} \hypertarget{axiom:OR-1}{}
{\tt \tiny [\verb]axiom:OR-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (A\ \lor\ B)$
\end{longtable}

\end{ax}


\begin{ax}[Disjunction Introduction Left\index{disjunction!introduction}]
\label{axiom:OR-2} \hypertarget{axiom:OR-2}{}
{\tt \tiny [\verb]axiom:OR-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (B\ \lor\ A)$
\end{longtable}

\end{ax}


\begin{ax}[Disjunction Elimination\index{disjunction!elimination}]
\label{axiom:OR-3} \hypertarget{axiom:OR-3}{}
{\tt \tiny [\verb]axiom:OR-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$
\end{longtable}

\end{ax}


\begin{ax}[Negation Introduction\index{negation!introduction}]
\label{axiom:NOT-1} \hypertarget{axiom:NOT-1}{}
{\tt \tiny [\verb]axiom:NOT-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$
\end{longtable}

\end{ax}


\begin{ax}[Negation Elimination\index{negation!elimination}]
\label{axiom:NOT-2} \hypertarget{axiom:NOT-2}{}
{\tt \tiny [\verb]axiom:NOT-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg A\ \rightarrow\ (A\ \rightarrow\ B)$
\end{longtable}

\end{ax}


\begin{ax}[Excluded Middle\index{negation!excluded middle}]
\label{axiom:NOT-3} \hypertarget{axiom:NOT-3}{}
{\tt \tiny [\verb]axiom:NOT-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \lor\ \neg A$
\end{longtable}

\end{ax}


\begin{ax}[Equivalence Elimination right\index{equivalence!elimination}]
\label{axiom:IFF-1} \hypertarget{axiom:IFF-1}{}
{\tt \tiny [\verb]axiom:IFF-1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \leftrightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ B)$
\end{longtable}

\end{ax}


\begin{ax}[Equivalence Elimination left\index{equivalence!elimination}]
\label{axiom:IFF-2} \hypertarget{axiom:IFF-2}{}
{\tt \tiny [\verb]axiom:IFF-2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \leftrightarrow\ B)\ \rightarrow\ (B\ \rightarrow\ A)$
\end{longtable}

\end{ax}


\begin{ax}[Equivalence Introduction\index{equivalence!introduction}]
\label{axiom:IFF-3} \hypertarget{axiom:IFF-3}{}
{\tt \tiny [\verb]axiom:IFF-3]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ A)\ \rightarrow\ (A\ \leftrightarrow\ B))$
\end{longtable}

\end{ax}


\par
If something is true for all $x$, it is true for any specific $y$.

\begin{ax}[Universal Instantiation\index{axiom!of universal instantiation}]
\label{axiom:universalInstantiation} \hypertarget{axiom:universalInstantiation}{}
{\tt \tiny [\verb]axiom:universalInstantiation]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\forall x\ \phi(x)\ \rightarrow\ \phi(y)$
\end{longtable}

\end{ax}


\par
If a predicate holds for some particular $y$, then there is an $x$ for which the predicate holds.

\begin{ax}[Existential Generalization\index{axiom!of existential generalization}]
\label{axiom:existencialGeneralization} \hypertarget{axiom:existencialGeneralization}{}
{\tt \tiny [\verb]axiom:existencialGeneralization]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\phi(y)\ \rightarrow\ \exists x\ \phi(x)$
\end{longtable}

\end{ax}


\section{Rules of Inference\index{rules!of predicate calculus}\index{rules!of inference}} \label{chapter3_section2} \hypertarget{chapter3_section2}{}
The following rules of inference enable us to obtain new true formulas from the axioms that are assumed to be true. From these new formulas we derive further formulas. So we can successively extend the set of true formulas.

\begin{rul}[Add true formula]
\label{rule:addProvenFormula} \hypertarget{rule:addProvenFormula}{}
{\tt \tiny [\verb]rule:addProvenFormula]]}

\par
{\em   Name: \verb]Add]  -  Version: \verb]0.01.00]}


Addition of an axiom, definition or already proven formula. We have to reference to the location of a true formula.
\end{rul}


\begin{rul}[Modus Ponens\index{Modus Ponens}]
\label{rule:modusPonens} \hypertarget{rule:modusPonens}{}
{\tt \tiny [\verb]rule:modusPonens]]}

\par
{\em   Name: \verb]MP]  -  Version: \verb]0.01.00]}


If both formulas $\alpha$ and $\alpha \rightarrow \beta$ are true, then we can conclude that $\beta$ is true as well.
\end{rul}


\begin{rul}[Replace Free Subject Variable]
\label{rule:replaceFree} \hypertarget{rule:replaceFree}{}
{\tt \tiny [\verb]rule:replaceFree]]}

\par
{\em   Name: \verb]SubstFree]  -  Version: \verb]0.01.00]}


We start with a true formula.
A free subject variable may be replaced by an arbitrary term, provided that the substituted term contains no subject variable that have a bound occurrence in the original formula. All occurrences of the free variable must be simultaneously replaced.
\end{rul}

The prohibition to use subject variables within the term that occur bound in the original formula has two reasons. First it ensures that the resulting formula is well-formed. Secondly it preserves the validity of the formula. Let us look at the following derivation.

\par
\begin{tabularx}{\linewidth}{rclX}
  $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(z,y)$ 
    & with \hyperlink{axiom:universalInstantiation}{axiom~15} \\
  $\forall x \ \exists y \ \phi(x, y)$ & $\rightarrow$ & $\exists y \ \phi(y,y)$ 
    & forbidden replacement: $z$ in $y$, despite $y$ is already bound \\
  $\forall x \ \exists y \ x \neq y$ & $\rightarrow$ & $\exists y \ \neq y$ 
    & replace $\neq$ for $\phi$
\end{tabularx}

\par
This last proposition is not valid in many models.


\begin{rul}[Rename Bound Subject Variable]
\label{rule:renameBound} \hypertarget{rule:renameBound}{}
{\tt \tiny [\verb]rule:renameBound]]}

\par
{\em   Name: \verb]Rename]  -  Version: \verb]0.01.00]}


We may replace a bound subject variable occurring in a formula by any other subject variable, provided that the new variable occurs not free in the original formula. If the variable to be replaced occurs in more than one scope, then the replacement needs to be made in one scope only.
\end{rul}


\begin{rul}[Replace Predicate Variable]
\label{rule:replacePred} \hypertarget{rule:replacePred}{}
{\tt \tiny [\verb]rule:replacePred]]}

\par
{\em   Name: \verb]SubstPred]  -  Version: \verb]0.01.00]}


Let $\alpha$ be a true formula that contains a predicate variable $p$ of arity $n$, let $x_1$, \ldots, $x_n$ be pairwise different subject variables and let $\beta(x_1, \ldots, x_n)$ be a formula where $x_1$, \ldots, $x_n$ are not bound. The formula $\beta(x_1, \ldots, x_n)$ must not contain all $x_1$, \ldots, $x_n$ as free subject variables. Furthermore it can also have other subject variables either free or bound.

If the following conditions are fulfilled, then a replacement of all occurrences of $p(t_1, \ldots, t_n)$ each with appropriate terms $t_1$, \ldots, $t_n$ in $\alpha$ by $\beta(t_1, \ldots, t_n)$ results in another true formula.

\begin{itemize}

\item
the free variables of $\beta(x_1, \ldots, x_n)$ without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$ 

\item 
each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains no bound variable of $\beta(x_1, \ldots, x_n)$ 

\item
the result of the substitution is a well-formed formula

\end{itemize}
\end{rul}

See III \S 5 in \cite{hilback}.

\par
The prohibition to use additional subject variables within the replacement formula that occur bound in the original formula assurs that the resulting formula is well-formed. Furthermore it preserves the validity of the formla. Take a look at the following derivation.

\par
\begin{tabularx}{\linewidth}{rclX}
  $ \phi(x)$                             & $\rightarrow$ & $\exists y \ \phi(y)$  
    & with \hyperlink{axiom:existencialGeneralization}{axiom~16} \\
  $ (\exists y \ y = y) \land \phi(x)$   & $\rightarrow$ & $\exists y \ \phi(y)$  
    &  \\
  $ \exists y \ (y = y \land \phi(x))$   & $\rightarrow$ & $\exists y \ \phi(y)$  
    &  \\
  $ \exists y \ (y = y \land x \neq y)$  & $\rightarrow$ & $\exists y \ y \neq y$  
    & forbidden replacment: $\phi(x)$ by $x \neq y$, despite $y$ is already bound \\
  $ \exists y \  x \neq y$  & $\rightarrow$ & $\exists y \ y \neq y$  
    &
\end{tabularx}

\par
The last proposition is not valid in many models.


\par
Analogous to \hyperlink{rule:replacePred}{rule~5} we can replace function variables too.

\begin{rul}[Replace Function Variable]
\label{rule:replaceFunct} \hypertarget{rule:replaceFunct}{}
{\tt \tiny [\verb]rule:replaceFunct]]}

\par
{\em   Name: \verb]SubstFun]  -  Version: \verb]0.01.00]}


Let $\alpha$ be an already proved formula that contains a function variable $\sigma$ of arity $n$, let $x_1$, \ldots, $x_n$ be pairwise different subject variables and let $\tau(x_1, \ldots, x_n)$ be an arbitrary term where $x_1$, \ldots, $x_n$ are not bound. 
The term $\tau(x_1, \ldots, x_n)$ must not contain all $x_1$, \ldots, $x_n$ as free subject variables. Furthermore it can also have other subject variables either free or bound. 

If the following conditions are fulfilled we can obtain a new true formula by replacing each occurrence of $\sigma(t_1, \ldots, t_n)$ with appropriate terms $t_1$, \ldots, $t_n$ in $\alpha$ by $\tau(t_1, \ldots, t_n)$.

\begin{itemize}

\item 
the free variables of $\tau(x_1, \ldots, x_n)$ without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$

\item
each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$ contains no bound variable of $\tau(x_1, \ldots, x_n)$

\item
the result of the substitution is a well-formed formula
                  
\end{itemize}
\end{rul}


\begin{rul}[Universal Generalization]
\label{rule:universalGeneralization} \hypertarget{rule:universalGeneralization}{}
{\tt \tiny [\verb]rule:universalGeneralization]]}

\par
{\em   Name: \verb]Universal]  -  Version: \verb]0.01.00]}


If $\alpha \rightarrow \beta(x_1)$ is a true formula and $\alpha$ does not contain the subject variable $x_1$, then $\alpha \rightarrow (\forall x_1~(\beta(x_1)))$ is a true 
formula too.
\end{rul}


\begin{rul}[Existential Generalization]
\label{rule:existentialGeneralization} \hypertarget{rule:existentialGeneralization}{}
{\tt \tiny [\verb]rule:existentialGeneralization]]}

\par
{\em   Name: \verb]Existential]  -  Version: \verb]0.01.00]}


If $\alpha(x_1) \rightarrow \beta$ is already proved to be true and $\beta$ does not contain the subject variable $x_1$, then $(\exists x_1~\alpha(x_1)) \rightarrow \beta$ is also a true formula.
\end{rul}



%% end of chapter Axioms and Rules of Inference

\chapter{Propositional Calculus} \label{chapter4} \hypertarget{chapter4}{}

In this chapter we introduce an importent new inference rule and develop the traditional results of propositional calculus.

\section{First Propositions} \label{chapter4_section1} \hypertarget{chapter4_section1}{}
Here we draw the first conclusions.

\begin{prop}
\label{proposition:implicationReflexive1} \hypertarget{proposition:implicationReflexive1}{}
{\tt \tiny [\verb]proposition:implicationReflexive1]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implicationReflexive1!1} \hypertarget{proposition:implicationReflexive1!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:THEN-1}{axiom~1}} \\ 
\label{proposition:implicationReflexive1!2} \hypertarget{proposition:implicationReflexive1!2}{\mbox{(2)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:THEN-2}{axiom~2}} \\ 
\label{proposition:implicationReflexive1!3} \hypertarget{proposition:implicationReflexive1!3}{\mbox{(3)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-2}{axiom~7}} \\ 
\label{proposition:implicationReflexive1!4} \hypertarget{proposition:implicationReflexive1!4}{\mbox{(4)}}  \ &  \ $A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $B\ \lor\ A$ in \hyperlink{proposition:implicationReflexive1!1}{(1)}} \\ 
\label{proposition:implicationReflexive1!5} \hypertarget{proposition:implicationReflexive1!5}{\mbox{(5)}}  \ &  \ $(A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ C))\ \rightarrow\ ((A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $B\ \lor\ A$ in \hyperlink{proposition:implicationReflexive1!2}{(2)}} \\ 
\label{proposition:implicationReflexive1!6} \hypertarget{proposition:implicationReflexive1!6}{\mbox{(6)}}  \ &  \ $(A\ \rightarrow\ ((B\ \lor\ A)\ \rightarrow\ A))\ \rightarrow\ ((A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ A))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implicationReflexive1!5}{(5)}} \\ 
\label{proposition:implicationReflexive1!7} \hypertarget{proposition:implicationReflexive1!7}{\mbox{(7)}}  \ &  \ $(A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ (A\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implicationReflexive1!6}{(6)}, \hyperlink{proposition:implicationReflexive1!4}{(4)}} \\ 
\label{proposition:implicationReflexive1!8} \hypertarget{proposition:implicationReflexive1!8}{\mbox{(8)}}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implicationReflexive1!7}{(7)}, \hyperlink{proposition:implicationReflexive1!3}{(3)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication2} \hypertarget{proposition:implication2}{}
{\tt \tiny [\verb]proposition:implication2]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \lor\ A)\ \rightarrow\ A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication2!1} \hypertarget{proposition:implication2!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{proposition:implicationReflexive1}{proposition~1}} \\ 
\label{proposition:implication2!2} \hypertarget{proposition:implication2!2}{\mbox{(2)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication2!3} \hypertarget{proposition:implication2!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((A\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ A)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication2!2}{(2)}} \\ 
\label{proposition:implication2!4} \hypertarget{proposition:implication2!4}{\mbox{(4)}}  \ &  \ $(A\ \rightarrow\ A)\ \rightarrow\ ((A\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ A)\ \rightarrow\ A))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implication2!3}{(3)}} \\ 
\label{proposition:implication2!5} \hypertarget{proposition:implication2!5}{\mbox{(5)}}  \ &  \ $(A\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ A)\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication2!4}{(4)}, \hyperlink{proposition:implication2!1}{(1)}} \\ 
\label{proposition:implication2!6} \hypertarget{proposition:implication2!6}{\mbox{(6)}}  \ &  \ $(A\ \lor\ A)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication2!5}{(5)}, \hyperlink{proposition:implication2!1}{(1)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication03} \hypertarget{proposition:implication03}{}
{\tt \tiny [\verb]proposition:implication03]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication03!1} \hypertarget{proposition:implication03!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ B)$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-1}{axiom~6}} \\ 
\label{proposition:implication03!2} \hypertarget{proposition:implication03!2}{\mbox{(2)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-2}{axiom~7}} \\ 
\label{proposition:implication03!3} \hypertarget{proposition:implication03!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication03!4} \hypertarget{proposition:implication03!4}{\mbox{(4)}}  \ &  \ $D\ \rightarrow\ (D\ \lor\ B)$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $A$ by $D$ in \hyperlink{proposition:implication03!1}{(1)}} \\ 
\label{proposition:implication03!5} \hypertarget{proposition:implication03!5}{\mbox{(5)}}  \ &  \ $(A\ \rightarrow\ (C\ \lor\ A))\ \rightarrow\ ((B\ \rightarrow\ (C\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (C\ \lor\ A)))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $C$ by $C\ \lor\ A$ in \hyperlink{proposition:implication03!3}{(3)}} \\ 
\label{proposition:implication03!6} \hypertarget{proposition:implication03!6}{\mbox{(6)}}  \ &  \ $D\ \rightarrow\ (D\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication03!4}{(4)}} \\ 
\label{proposition:implication03!7} \hypertarget{proposition:implication03!7}{\mbox{(7)}}  \ &  \ $(A\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((B\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $C$ by $B$ in \hyperlink{proposition:implication03!5}{(5)}} \\ 
\label{proposition:implication03!8} \hypertarget{proposition:implication03!8}{\mbox{(8)}}  \ &  \ $(B\ \rightarrow\ (B\ \lor\ A))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A))$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication03!7}{(7)}, \hyperlink{proposition:implication03!2}{(2)}} \\ 
\label{proposition:implication03!9} \hypertarget{proposition:implication03!9}{\mbox{(9)}}  \ &  \ $B\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $D$ by $B$ in \hyperlink{proposition:implication03!6}{(6)}} \\ 
\label{proposition:implication03!10} \hypertarget{proposition:implication03!10}{\mbox{(10)}}  \ &  \ $(A\ \lor\ B)\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication03!8}{(8)}, \hyperlink{proposition:implication03!9}{(9)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication04} \hypertarget{proposition:implication04}{}
{\tt \tiny [\verb]proposition:implication04]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg (A\ \land\ \neg A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication04!1} \hypertarget{proposition:implication04!1}{\mbox{(1)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication04!2} \hypertarget{proposition:implication04!2}{\mbox{(2)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication04!3} \hypertarget{proposition:implication04!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:addProvenFormula}{Add} \hyperlink{axiom:NOT-1}{axiom~9}} \\ 
\label{proposition:implication04!4} \hypertarget{proposition:implication04!4}{\mbox{(4)}}  \ &  \ $(A\ \land\ \neg A)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication04!1}{(1)}} \\ 
\label{proposition:implication04!5} \hypertarget{proposition:implication04!5}{\mbox{(5)}}  \ &  \ $(A\ \land\ \neg A)\ \rightarrow\ \neg A$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication04!2}{(2)}} \\ 
\label{proposition:implication04!6} \hypertarget{proposition:implication04!6}{\mbox{(6)}}  \ &  \ $((A\ \land\ \neg A)\ \rightarrow\ B)\ \rightarrow\ (((A\ \land\ \neg A)\ \rightarrow\ \neg B)\ \rightarrow\ \neg (A\ \land\ \neg A))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $A$ by $A\ \land\ \neg A$ in \hyperlink{proposition:implication04!3}{(3)}} \\ 
\label{proposition:implication04!7} \hypertarget{proposition:implication04!7}{\mbox{(7)}}  \ &  \ $((A\ \land\ \neg A)\ \rightarrow\ A)\ \rightarrow\ (((A\ \land\ \neg A)\ \rightarrow\ \neg A)\ \rightarrow\ \neg (A\ \land\ \neg A))$ \ &  \ {\tiny \hyperlink{rule:replacePred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication04!6}{(6)}} \\ 
\label{proposition:implication04!8} \hypertarget{proposition:implication04!8}{\mbox{(8)}}  \ &  \ $((A\ \land\ \neg A)\ \rightarrow\ \neg A)\ \rightarrow\ \neg (A\ \land\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication04!7}{(7)}, \hyperlink{proposition:implication04!4}{(4)}} \\ 
\label{proposition:implication04!9} \hypertarget{proposition:implication04!9}{\mbox{(9)}}  \ &  \ $\neg (A\ \land\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:modusPonens}{MP} \hyperlink{proposition:implication04!8}{(8)}, \hyperlink{proposition:implication04!5}{(5)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\section{Deduction Theorem\index{deduction theorem}} \label{chapter4_section2} \hypertarget{chapter4_section2}{}
We prove the deduction theorem. This leads to the new rule \emph{Conditional Proof}.

\par
If we can prove $B$ by assuming $A$ as a hypothesis then we have proved $A \rightarrow B$. This reasoning is justified by the so-called \emph{deduction theorem}. The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However our use of proposition variables and substitution rules make difficulties. We have to restrict the allowed inference rules to get a simular result.

\begin{rul}
\label{rule:CP} \hypertarget{rule:CP}{}
{\tt \tiny [\verb]rule:CP]]}

\par
{\em   Name: \verb]CP]  -  Version: \verb]0.02.00]}


We have the well-formed formula $\alpha$ and add it as a new proof line. Now we modify the existing inference rules. We can add a further proof line $\beta$ if $\alpha \rightarrow \beta$ is a well-formed formula and the usage of a previous inference rule with the following restrictions justifies the addition:
for \hyperlink{rule:replaceFree}{rule~3} occurs the replaced free variable not in $\alpha$, for \hyperlink{rule:replacePred}{rule~5} occurs the replaced predicate variable not in $\alpha$, for \hyperlink{rule:replaceFunct}{rule~6} occurs the replaced function variable not in $\alpha$.
\end{rul}
Based on: 
 \hyperlink{axiom:THEN-1}{axiom~1} \hyperlink{axiom:THEN-2}{axiom~2}
The following rules have to be extended.

\par
\label{rule:CP!MP} \hypertarget{rule:CP!MP}{}
{\em   Name: \verb]MP]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:modusPonens}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\par
\label{rule:CP!Add} \hypertarget{rule:CP!Add}{}
{\em   Name: \verb]Add]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:addProvenFormula}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\par
\label{rule:CP!Rename} \hypertarget{rule:CP!Rename}{}
{\em   Name: \verb]Rename]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:renameBound}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\par
\label{rule:CP!SubstFree} \hypertarget{rule:CP!SubstFree}{}
{\em   Name: \verb]SubstFree]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:replaceFree}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\par
\label{rule:CP!SubstPred} \hypertarget{rule:CP!SubstPred}{}
{\em   Name: \verb]SubstPred]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:replacePred}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\par
\label{rule:CP!SubstFun} \hypertarget{rule:CP!SubstFun}{}
{\em   Name: \verb]SubstFun]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:replaceFunct}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\par
\label{rule:CP!Universal} \hypertarget{rule:CP!Universal}{}
{\em   Name: \verb]Universal]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:universalGeneralization}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\par
\label{rule:CP!Existential} \hypertarget{rule:CP!Existential}{}
{\em   Name: \verb]Existential]  -  Version: \verb]0.02.00]  -  Old Version: \hyperlink{rule:existentialGeneralization}{0.01.00}}

See \hyperlink{rule:CP}{rule~9}.


\begin{proof}
TODO 20110613 m31
\end{proof}

The deduction theorem enables us to prove propositions more easier in the next sections.


\section{Propositions about implication} \label{chapter4_section3} \hypertarget{chapter4_section3}{}
We use \hyperlink{rule:CP}{rule~9} to derive more propositions containing only the implication operator.

\begin{prop}
\label{proposition:implication10} \hypertarget{proposition:implication10}{}
{\tt \tiny [\verb]proposition:implication10]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (A\ \rightarrow\ B))\ \rightarrow\ (A\ \rightarrow\ B)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication10!1} \hypertarget{proposition:implication10!1}{\mbox{(1)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication10!2} \hypertarget{proposition:implication10!2}{\mbox{(2)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication10!3} \hypertarget{proposition:implication10!3}{\mbox{(3)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication10!1}{(1)}, \hyperlink{proposition:implication10!2}{(2)}} \\ 
\label{proposition:implication10!4} \hypertarget{proposition:implication10!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication10!3}{(3)}, \hyperlink{proposition:implication10!2}{(2)}} \\ 
\label{proposition:implication10!5} \hypertarget{proposition:implication10!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication10!6} \hypertarget{proposition:implication10!6}{\mbox{(6)}}  \ &  \ $(A\ \rightarrow\ (A\ \rightarrow\ B))\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication11} \hypertarget{proposition:implication11}{}
{\tt \tiny [\verb]proposition:implication11]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication11!1} \hypertarget{proposition:implication11!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{axiom~1}} \\ 
\label{proposition:implication11!2} \hypertarget{proposition:implication11!2}{\mbox{(2)}}  \ &  \ $D\ \rightarrow\ (B\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $D$ in \hyperlink{proposition:implication11!1}{(1)}} \\ 
\label{proposition:implication11!3} \hypertarget{proposition:implication11!3}{\mbox{(3)}}  \ &  \ $D\ \rightarrow\ (A\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication11!2}{(2)}} \\ 
\label{proposition:implication11!4} \hypertarget{proposition:implication11!4}{\mbox{(4)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $B$ in \hyperlink{proposition:implication11!3}{(3)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication11!5} \hypertarget{proposition:implication11!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication11!6} \hypertarget{proposition:implication11!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication11!7} \hypertarget{proposition:implication11!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication11!8} \hypertarget{proposition:implication11!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication11!4}{(4)}, \hyperlink{proposition:implication11!7}{(7)}} \\ 
\label{proposition:implication11!9} \hypertarget{proposition:implication11!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication11!5}{(5)}, \hyperlink{proposition:implication11!8}{(8)}} \\ 
\label{proposition:implication11!10} \hypertarget{proposition:implication11!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication11!9}{(9)}, \hyperlink{proposition:implication11!6}{(6)}} \\ 
\label{proposition:implication11!11} \hypertarget{proposition:implication11!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication11!12} \hypertarget{proposition:implication11!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication11!13} \hypertarget{proposition:implication11!13}{\mbox{(13)}}  \ &  \ $((A\ \rightarrow\ B)\ \rightarrow\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication12} \hypertarget{proposition:implication12}{}
{\tt \tiny [\verb]proposition:implication12]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication12!1} \hypertarget{proposition:implication12!1}{\mbox{(1)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication12!2} \hypertarget{proposition:implication12!2}{\mbox{(2)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication12!3} \hypertarget{proposition:implication12!3}{\mbox{(3)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication12!4} \hypertarget{proposition:implication12!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication12!1}{(1)}, \hyperlink{proposition:implication12!3}{(3)}} \\ 
\label{proposition:implication12!5} \hypertarget{proposition:implication12!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication12!2}{(2)}, \hyperlink{proposition:implication12!4}{(4)}} \\ 
\label{proposition:implication12!6} \hypertarget{proposition:implication12!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication12!7} \hypertarget{proposition:implication12!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}$(B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication12!8} \hypertarget{proposition:implication12!8}{\mbox{(8)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication13} \hypertarget{proposition:implication13}{}
{\tt \tiny [\verb]proposition:implication13]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ (A\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication13!1} \hypertarget{proposition:implication13!1}{\mbox{(1)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication13!2} \hypertarget{proposition:implication13!2}{\mbox{(2)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication13!3} \hypertarget{proposition:implication13!3}{\mbox{(3)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication13!4} \hypertarget{proposition:implication13!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication13!1}{(1)}, \hyperlink{proposition:implication13!3}{(3)}} \\ 
\label{proposition:implication13!5} \hypertarget{proposition:implication13!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication13!4}{(4)}, \hyperlink{proposition:implication13!2}{(2)}} \\ 
\label{proposition:implication13!6} \hypertarget{proposition:implication13!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication13!7} \hypertarget{proposition:implication13!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication13!8} \hypertarget{proposition:implication13!8}{\mbox{(8)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\section{Propositions about conjunction} \label{chapter4_section4} \hypertarget{chapter4_section4}{}
We use \hyperlink{rule:CP}{rule~9} to derive more propositions containing the conjunction operator.

\begin{prop}
\label{proposition:implication14} \hypertarget{proposition:implication14}{}
{\tt \tiny [\verb]proposition:implication14]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (A\ \land\ A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication14!1} \hypertarget{proposition:implication14!1}{\mbox{(1)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication14!2} \hypertarget{proposition:implication14!2}{\mbox{(2)}}  \ &  \ $A\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ A))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication14!1}{(1)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication14!3} \hypertarget{proposition:implication14!3}{\mbox{(3)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication14!4} \hypertarget{proposition:implication14!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (A\ \land\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication14!2}{(2)}, \hyperlink{proposition:implication14!3}{(3)}} \\ 
\label{proposition:implication14!5} \hypertarget{proposition:implication14!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}$A\ \land\ A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication14!4}{(4)}, \hyperlink{proposition:implication14!3}{(3)}} \\ 
\label{proposition:implication14!6} \hypertarget{proposition:implication14!6}{\mbox{(6)}}  \ &  \ $A\ \rightarrow\ (A\ \land\ A)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:AND-3b} \hypertarget{proposition:AND-3b}{}
{\tt \tiny [\verb]proposition:AND-3b]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ (B\ \rightarrow\ (A\ \land\ B))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:AND-3b!1} \hypertarget{proposition:AND-3b!1}{\mbox{(1)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication13}{proposition~8}} \\ 
\label{proposition:AND-3b!2} \hypertarget{proposition:AND-3b!2}{\mbox{(2)}}  \ &  \ $(A\ \rightarrow\ (D\ \rightarrow\ C))\ \rightarrow\ (D\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $D$ in \hyperlink{proposition:AND-3b!1}{(1)}} \\ 
\label{proposition:AND-3b!3} \hypertarget{proposition:AND-3b!3}{\mbox{(3)}}  \ &  \ $(B\ \rightarrow\ (D\ \rightarrow\ C))\ \rightarrow\ (D\ \rightarrow\ (B\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:AND-3b!2}{(2)}} \\ 
\label{proposition:AND-3b!4} \hypertarget{proposition:AND-3b!4}{\mbox{(4)}}  \ &  \ $(B\ \rightarrow\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $A$ in \hyperlink{proposition:AND-3b!3}{(3)}} \\ 
\label{proposition:AND-3b!5} \hypertarget{proposition:AND-3b!5}{\mbox{(5)}}  \ &  \ $(B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B)))\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ (A\ \land\ B)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \land\ B$ in \hyperlink{proposition:AND-3b!4}{(4)}} \\ 
\label{proposition:AND-3b!6} \hypertarget{proposition:AND-3b!6}{\mbox{(6)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:AND-3b!7} \hypertarget{proposition:AND-3b!7}{\mbox{(7)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:AND-3b!5}{(5)}, \hyperlink{proposition:AND-3b!6}{(6)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication15} \hypertarget{proposition:implication15}{}
{\tt \tiny [\verb]proposition:implication15]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication15!1} \hypertarget{proposition:implication15!1}{\mbox{(1)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication15!2} \hypertarget{proposition:implication15!2}{\mbox{(2)}}  \ &  \ $(A\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \rightarrow\ C$ in \hyperlink{proposition:implication15!1}{(1)}} \\ 
\label{proposition:implication15!3} \hypertarget{proposition:implication15!3}{\mbox{(3)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication15!2}{(2)}} \\ 
\label{proposition:implication15!4} \hypertarget{proposition:implication15!4}{\mbox{(4)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication15!5} \hypertarget{proposition:implication15!5}{\mbox{(5)}}  \ &  \ $(A\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \rightarrow\ C$ in \hyperlink{proposition:implication15!4}{(4)}} \\ 
\label{proposition:implication15!6} \hypertarget{proposition:implication15!6}{\mbox{(6)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication15!5}{(5)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication15!7} \hypertarget{proposition:implication15!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication15!8} \hypertarget{proposition:implication15!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!3}{(3)}, \hyperlink{proposition:implication15!7}{(7)}} \\ 
\label{proposition:implication15!9} \hypertarget{proposition:implication15!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!6}{(6)}, \hyperlink{proposition:implication15!7}{(7)}} \\ 
\label{proposition:implication15!10} \hypertarget{proposition:implication15!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication12}{proposition~7}} \\ 
\label{proposition:implication15!11} \hypertarget{proposition:implication15!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$(B\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!10}{(10)}, \hyperlink{proposition:implication15!8}{(8)}} \\ 
\label{proposition:implication15!12} \hypertarget{proposition:implication15!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication15!11}{(11)}, \hyperlink{proposition:implication15!9}{(9)}} \\ 
\label{proposition:implication15!13} \hypertarget{proposition:implication15!13}{\mbox{(13)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication17} \hypertarget{proposition:implication17}{}
{\tt \tiny [\verb]proposition:implication17]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C)))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication17!1} \hypertarget{proposition:implication17!1}{\mbox{(1)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication17!2} \hypertarget{proposition:implication17!2}{\mbox{(2)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication17!1}{(1)}} \\ 
\label{proposition:implication17!3} \hypertarget{proposition:implication17!3}{\mbox{(3)}}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication17!2}{(2)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication17!4} \hypertarget{proposition:implication17!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication17!5} \hypertarget{proposition:implication17!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication17!6} \hypertarget{proposition:implication17!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication17!7} \hypertarget{proposition:implication17!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!5}{(5)}, \hyperlink{proposition:implication17!6}{(6)}} \\ 
\label{proposition:implication17!8} \hypertarget{proposition:implication17!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!3}{(3)}, \hyperlink{proposition:implication17!7}{(7)}} \\ 
\label{proposition:implication17!9} \hypertarget{proposition:implication17!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!4}{(4)}, \hyperlink{proposition:implication17!6}{(6)}} \\ 
\label{proposition:implication17!10} \hypertarget{proposition:implication17!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication17!8}{(8)}, \hyperlink{proposition:implication17!9}{(9)}} \\ 
\label{proposition:implication17!11} \hypertarget{proposition:implication17!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication17!12} \hypertarget{proposition:implication17!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication17!13} \hypertarget{proposition:implication17!13}{\mbox{(13)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C)))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication18} \hypertarget{proposition:implication18}{}
{\tt \tiny [\verb]proposition:implication18]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \land\ C)\ \rightarrow\ (B\ \land\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication18!1} \hypertarget{proposition:implication18!1}{\mbox{(1)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication18!2} \hypertarget{proposition:implication18!2}{\mbox{(2)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication18!1}{(1)}} \\ 
\label{proposition:implication18!3} \hypertarget{proposition:implication18!3}{\mbox{(3)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication18!4} \hypertarget{proposition:implication18!4}{\mbox{(4)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication18!3}{(3)}} \\ 
\label{proposition:implication18!5} \hypertarget{proposition:implication18!5}{\mbox{(5)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication18!6} \hypertarget{proposition:implication18!6}{\mbox{(6)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication18!5}{(5)}} \\ 
\label{proposition:implication18!7} \hypertarget{proposition:implication18!7}{\mbox{(7)}}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication18!6}{(6)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication18!8} \hypertarget{proposition:implication18!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication18!9} \hypertarget{proposition:implication18!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \land\ C$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication18!10} \hypertarget{proposition:implication18!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!2}{(2)}, \hyperlink{proposition:implication18!9}{(9)}} \\ 
\label{proposition:implication18!11} \hypertarget{proposition:implication18!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!8}{(8)}, \hyperlink{proposition:implication18!10}{(10)}} \\ 
\label{proposition:implication18!12} \hypertarget{proposition:implication18!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!4}{(4)}, \hyperlink{proposition:implication18!9}{(9)}} \\ 
\label{proposition:implication18!13} \hypertarget{proposition:implication18!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!7}{(7)}, \hyperlink{proposition:implication18!12}{(12)}} \\ 
\label{proposition:implication18!14} \hypertarget{proposition:implication18!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication18!13}{(13)}, \hyperlink{proposition:implication18!11}{(11)}} \\ 
\label{proposition:implication18!15} \hypertarget{proposition:implication18!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}$(A\ \land\ C)\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication18!16} \hypertarget{proposition:implication18!16}{\mbox{(16)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \land\ C)\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication19} \hypertarget{proposition:implication19}{}
{\tt \tiny [\verb]proposition:implication19]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \land\ B)\ \rightarrow\ (B\ \land\ A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication19!1} \hypertarget{proposition:implication19!1}{\mbox{(1)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication19!2} \hypertarget{proposition:implication19!2}{\mbox{(2)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication19!1}{(1)}} \\ 
\label{proposition:implication19!3} \hypertarget{proposition:implication19!3}{\mbox{(3)}}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication19!2}{(2)}} \\ 
\label{proposition:implication19!4} \hypertarget{proposition:implication19!4}{\mbox{(4)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ A))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implication19!3}{(3)}} \\ 
\label{proposition:implication19!5} \hypertarget{proposition:implication19!5}{\mbox{(5)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication19!6} \hypertarget{proposition:implication19!6}{\mbox{(6)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication19!7} \hypertarget{proposition:implication19!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication19!8} \hypertarget{proposition:implication19!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!5}{(5)}, \hyperlink{proposition:implication19!7}{(7)}} \\ 
\label{proposition:implication19!9} \hypertarget{proposition:implication19!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ (B\ \land\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!4}{(4)}, \hyperlink{proposition:implication19!8}{(8)}} \\ 
\label{proposition:implication19!10} \hypertarget{proposition:implication19!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!6}{(6)}, \hyperlink{proposition:implication19!7}{(7)}} \\ 
\label{proposition:implication19!11} \hypertarget{proposition:implication19!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$B\ \land\ A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication19!9}{(9)}, \hyperlink{proposition:implication19!10}{(10)}} \\ 
\label{proposition:implication19!12} \hypertarget{proposition:implication19!12}{\mbox{(12)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ (B\ \land\ A)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication20} \hypertarget{proposition:implication20}{}
{\tt \tiny [\verb]proposition:implication20]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication20!1} \hypertarget{proposition:implication20!1}{\mbox{(1)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication20!2} \hypertarget{proposition:implication20!2}{\mbox{(2)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication20!3} \hypertarget{proposition:implication20!3}{\mbox{(3)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication20!4} \hypertarget{proposition:implication20!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!3}{(3)}, \hyperlink{proposition:implication20!2}{(2)}} \\ 
\label{proposition:implication20!5} \hypertarget{proposition:implication20!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication20!6} \hypertarget{proposition:implication20!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!5}{(5)}, \hyperlink{proposition:implication20!2}{(2)}} \\ 
\label{proposition:implication20!7} \hypertarget{proposition:implication20!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!1}{(1)}, \hyperlink{proposition:implication20!4}{(4)}} \\ 
\label{proposition:implication20!8} \hypertarget{proposition:implication20!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication20!7}{(7)}, \hyperlink{proposition:implication20!6}{(6)}} \\ 
\label{proposition:implication20!9} \hypertarget{proposition:implication20!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication20!10} \hypertarget{proposition:implication20!10}{\mbox{(10)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication21} \hypertarget{proposition:implication21}{}
{\tt \tiny [\verb]proposition:implication21]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \land\ B)\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication21!1} \hypertarget{proposition:implication21!1}{\mbox{(1)}}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ C$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication21!2} \hypertarget{proposition:implication21!2}{\mbox{(2)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication21!3} \hypertarget{proposition:implication21!3}{\mbox{(3)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
 \ &  \ \mbox{\qquad}\mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication21!4} \hypertarget{proposition:implication21!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication21!5} \hypertarget{proposition:implication21!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ (A\ \land\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication21!3}{(3)}, \hyperlink{proposition:implication21!4}{(4)}} \\ 
\label{proposition:implication21!6} \hypertarget{proposition:implication21!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication21!5}{(5)}, \hyperlink{proposition:implication21!2}{(2)}} \\ 
\label{proposition:implication21!7} \hypertarget{proposition:implication21!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication21!1}{(1)}, \hyperlink{proposition:implication21!6}{(6)}} \\ 
\label{proposition:implication21!8} \hypertarget{proposition:implication21!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication21!9} \hypertarget{proposition:implication21!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication21!10} \hypertarget{proposition:implication21!10}{\mbox{(10)}}  \ &  \ $((A\ \land\ B)\ \rightarrow\ C)\ \rightarrow\ (A\ \rightarrow\ (B\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication25} \hypertarget{proposition:implication25}{}
{\tt \tiny [\verb]proposition:implication25]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication25!1} \hypertarget{proposition:implication25!1}{\mbox{(1)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication25!2} \hypertarget{proposition:implication25!2}{\mbox{(2)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication25!1}{(1)}} \\ 
\label{proposition:implication25!3} \hypertarget{proposition:implication25!3}{\mbox{(3)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ C)\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication25!2}{(2)}} \\ 
\label{proposition:implication25!4} \hypertarget{proposition:implication25!4}{\mbox{(4)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \rightarrow\ C$ in \hyperlink{proposition:implication25!3}{(3)}} \\ 
\label{proposition:implication25!5} \hypertarget{proposition:implication25!5}{\mbox{(5)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication25!6} \hypertarget{proposition:implication25!6}{\mbox{(6)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication25!5}{(5)}} \\ 
\label{proposition:implication25!7} \hypertarget{proposition:implication25!7}{\mbox{(7)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication25!6}{(6)}} \\ 
\label{proposition:implication25!8} \hypertarget{proposition:implication25!8}{\mbox{(8)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \rightarrow\ C$ in \hyperlink{proposition:implication25!7}{(7)}} \\ 
\label{proposition:implication25!9} \hypertarget{proposition:implication25!9}{\mbox{(9)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication25!10} \hypertarget{proposition:implication25!10}{\mbox{(10)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication25!9}{(9)}} \\ 
\label{proposition:implication25!11} \hypertarget{proposition:implication25!11}{\mbox{(11)}}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication25!10}{(10)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication25!12} \hypertarget{proposition:implication25!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C)$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication25!13} \hypertarget{proposition:implication25!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!4}{(4)}, \hyperlink{proposition:implication25!12}{(12)}} \\ 
\label{proposition:implication25!14} \hypertarget{proposition:implication25!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!8}{(8)}, \hyperlink{proposition:implication25!12}{(12)}} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication25!15} \hypertarget{proposition:implication25!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication25!16} \hypertarget{proposition:implication25!16}{\mbox{(16)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!13}{(13)}, \hyperlink{proposition:implication25!15}{(15)}} \\ 
\label{proposition:implication25!17} \hypertarget{proposition:implication25!17}{\mbox{(17)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!14}{(14)}, \hyperlink{proposition:implication25!15}{(15)}} \\ 
\label{proposition:implication25!18} \hypertarget{proposition:implication25!18}{\mbox{(18)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!11}{(11)}, \hyperlink{proposition:implication25!17}{(17)}} \\ 
\label{proposition:implication25!19} \hypertarget{proposition:implication25!19}{\mbox{(19)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication25!18}{(18)}, \hyperlink{proposition:implication25!16}{(16)}} \\ 
\label{proposition:implication25!20} \hypertarget{proposition:implication25!20}{\mbox{(20)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication25!21} \hypertarget{proposition:implication25!21}{\mbox{(21)}}  \ &  \ $((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))\ \rightarrow\ (A\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication26} \hypertarget{proposition:implication26}{}
{\tt \tiny [\verb]proposition:implication26]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ (B\ \land\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication26!1} \hypertarget{proposition:implication26!1}{\mbox{(1)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication26!2} \hypertarget{proposition:implication26!2}{\mbox{(2)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication26!1}{(1)}} \\ 
\label{proposition:implication26!3} \hypertarget{proposition:implication26!3}{\mbox{(3)}}  \ &  \ $(B\ \land\ C)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication26!2}{(2)}} \\ 
\label{proposition:implication26!4} \hypertarget{proposition:implication26!4}{\mbox{(4)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication26!5} \hypertarget{proposition:implication26!5}{\mbox{(5)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication26!4}{(4)}} \\ 
\label{proposition:implication26!6} \hypertarget{proposition:implication26!6}{\mbox{(6)}}  \ &  \ $(B\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication26!5}{(5)}} \\ 
\label{proposition:implication26!7} \hypertarget{proposition:implication26!7}{\mbox{(7)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication26!8} \hypertarget{proposition:implication26!8}{\mbox{(8)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication26!7}{(7)}} \\ 
\label{proposition:implication26!9} \hypertarget{proposition:implication26!9}{\mbox{(9)}}  \ &  \ $C\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ B$ in \hyperlink{proposition:implication26!8}{(8)}} \\ 
\label{proposition:implication26!10} \hypertarget{proposition:implication26!10}{\mbox{(10)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \rightarrow\ C$ in \hyperlink{proposition:implication26!9}{(9)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication26!11} \hypertarget{proposition:implication26!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication26!12} \hypertarget{proposition:implication26!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication26!13} \hypertarget{proposition:implication26!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!11}{(11)}, \hyperlink{proposition:implication26!12}{(12)}} \\ 
\label{proposition:implication26!14} \hypertarget{proposition:implication26!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!3}{(3)}, \hyperlink{proposition:implication26!13}{(13)}} \\ 
\label{proposition:implication26!15} \hypertarget{proposition:implication26!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Conclusion} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication26!16} \hypertarget{proposition:implication26!16}{\mbox{(16)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication26!17} \hypertarget{proposition:implication26!17}{\mbox{(17)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!11}{(11)}, \hyperlink{proposition:implication26!16}{(16)}} \\ 
\label{proposition:implication26!18} \hypertarget{proposition:implication26!18}{\mbox{(18)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!6}{(6)}, \hyperlink{proposition:implication26!17}{(17)}} \\ 
\label{proposition:implication26!19} \hypertarget{proposition:implication26!19}{\mbox{(19)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ C$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication26!20} \hypertarget{proposition:implication26!20}{\mbox{(20)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!10}{(10)}, \hyperlink{proposition:implication26!19}{(19)}} \\ 
\label{proposition:implication26!21} \hypertarget{proposition:implication26!21}{\mbox{(21)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication26!20}{(20)}, \hyperlink{proposition:implication26!15}{(15)}} \\ 
\label{proposition:implication26!22} \hypertarget{proposition:implication26!22}{\mbox{(22)}}  \ &  \ $(A\ \rightarrow\ (B\ \land\ C))\ \rightarrow\ ((A\ \rightarrow\ B)\ \land\ (A\ \rightarrow\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication27} \hypertarget{proposition:implication27}{}
{\tt \tiny [\verb]proposition:implication27]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \land\ B)\ \land\ C)\ \rightarrow\ (A\ \land\ (B\ \land\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication27!1} \hypertarget{proposition:implication27!1}{\mbox{(1)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication27!2} \hypertarget{proposition:implication27!2}{\mbox{(2)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication27!1}{(1)}} \\ 
\label{proposition:implication27!3} \hypertarget{proposition:implication27!3}{\mbox{(3)}}  \ &  \ $((A\ \land\ B)\ \land\ C)\ \rightarrow\ (A\ \land\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \land\ B$ in \hyperlink{proposition:implication27!2}{(2)}} \\ 
\label{proposition:implication27!4} \hypertarget{proposition:implication27!4}{\mbox{(4)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication27!5} \hypertarget{proposition:implication27!5}{\mbox{(5)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication27!4}{(4)}} \\ 
\label{proposition:implication27!6} \hypertarget{proposition:implication27!6}{\mbox{(6)}}  \ &  \ $((A\ \land\ B)\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \land\ B$ in \hyperlink{proposition:implication27!5}{(5)}} \\ 
\label{proposition:implication27!7} \hypertarget{proposition:implication27!7}{\mbox{(7)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication27!8} \hypertarget{proposition:implication27!8}{\mbox{(8)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication27!7}{(7)}} \\ 
\label{proposition:implication27!9} \hypertarget{proposition:implication27!9}{\mbox{(9)}}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ (B\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication27!8}{(8)}} \\ 
\label{proposition:implication27!10} \hypertarget{proposition:implication27!10}{\mbox{(10)}}  \ &  \ $(B\ \land\ C)\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ (B\ \land\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \land\ C$ in \hyperlink{proposition:implication27!7}{(7)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication27!11} \hypertarget{proposition:implication27!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \land\ C$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication27!12} \hypertarget{proposition:implication27!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!3}{(3)}, \hyperlink{proposition:implication27!11}{(11)}} \\ 
\label{proposition:implication27!13} \hypertarget{proposition:implication27!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!1}{(1)}, \hyperlink{proposition:implication27!12}{(12)}} \\ 
\label{proposition:implication27!14} \hypertarget{proposition:implication27!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!4}{(4)}, \hyperlink{proposition:implication27!12}{(12)}} \\ 
\label{proposition:implication27!15} \hypertarget{proposition:implication27!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!6}{(6)}, \hyperlink{proposition:implication27!11}{(11)}} \\ 
\label{proposition:implication27!16} \hypertarget{proposition:implication27!16}{\mbox{(16)}}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!9}{(9)}, \hyperlink{proposition:implication27!15}{(15)}} \\ 
\label{proposition:implication27!17} \hypertarget{proposition:implication27!17}{\mbox{(17)}}  \ &  \ \mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!16}{(16)}, \hyperlink{proposition:implication27!14}{(14)}} \\ 
\label{proposition:implication27!18} \hypertarget{proposition:implication27!18}{\mbox{(18)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (A\ \land\ (B\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!10}{(10)}, \hyperlink{proposition:implication27!17}{(17)}} \\ 
\label{proposition:implication27!19} \hypertarget{proposition:implication27!19}{\mbox{(19)}}  \ &  \ \mbox{\qquad}$A\ \land\ (B\ \land\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication27!18}{(18)}, \hyperlink{proposition:implication27!13}{(13)}} \\ 
\label{proposition:implication27!20} \hypertarget{proposition:implication27!20}{\mbox{(20)}}  \ &  \ $((A\ \land\ B)\ \land\ C)\ \rightarrow\ (A\ \land\ (B\ \land\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication28} \hypertarget{proposition:implication28}{}
{\tt \tiny [\verb]proposition:implication28]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \land\ (B\ \land\ C))\ \rightarrow\ ((A\ \land\ B)\ \land\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication28!1} \hypertarget{proposition:implication28!1}{\mbox{(1)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication28!2} \hypertarget{proposition:implication28!2}{\mbox{(2)}}  \ &  \ $(A\ \land\ (B\ \land\ C))\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \land\ C$ in \hyperlink{proposition:implication28!1}{(1)}} \\ 
\label{proposition:implication28!3} \hypertarget{proposition:implication28!3}{\mbox{(3)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication28!1}{(1)}} \\ 
\label{proposition:implication28!4} \hypertarget{proposition:implication28!4}{\mbox{(4)}}  \ &  \ $(B\ \land\ C)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication28!3}{(3)}} \\ 
\label{proposition:implication28!5} \hypertarget{proposition:implication28!5}{\mbox{(5)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication28!6} \hypertarget{proposition:implication28!6}{\mbox{(6)}}  \ &  \ $(A\ \land\ (B\ \land\ C))\ \rightarrow\ (B\ \land\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \land\ C$ in \hyperlink{proposition:implication28!5}{(5)}} \\ 
\label{proposition:implication28!7} \hypertarget{proposition:implication28!7}{\mbox{(7)}}  \ &  \ $(A\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication28!5}{(5)}} \\ 
\label{proposition:implication28!8} \hypertarget{proposition:implication28!8}{\mbox{(8)}}  \ &  \ $(B\ \land\ C)\ \rightarrow\ C$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication28!7}{(7)}} \\ 
\label{proposition:implication28!9} \hypertarget{proposition:implication28!9}{\mbox{(9)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication28!10} \hypertarget{proposition:implication28!10}{\mbox{(10)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication28!9}{(9)}} \\ 
\label{proposition:implication28!11} \hypertarget{proposition:implication28!11}{\mbox{(11)}}  \ &  \ $C\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ ((A\ \land\ B)\ \land\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \land\ B$ in \hyperlink{proposition:implication28!10}{(10)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication28!12} \hypertarget{proposition:implication28!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$A\ \land\ (B\ \land\ C)$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication28!13} \hypertarget{proposition:implication28!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!2}{(2)}, \hyperlink{proposition:implication28!12}{(12)}} \\ 
\label{proposition:implication28!14} \hypertarget{proposition:implication28!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$B\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!6}{(6)}, \hyperlink{proposition:implication28!12}{(12)}} \\ 
\label{proposition:implication28!15} \hypertarget{proposition:implication28!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!4}{(4)}, \hyperlink{proposition:implication28!14}{(14)}} \\ 
\label{proposition:implication28!16} \hypertarget{proposition:implication28!16}{\mbox{(16)}}  \ &  \ \mbox{\qquad}$C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!8}{(8)}, \hyperlink{proposition:implication28!14}{(14)}} \\ 
\label{proposition:implication28!17} \hypertarget{proposition:implication28!17}{\mbox{(17)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (A\ \land\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!9}{(9)}, \hyperlink{proposition:implication28!15}{(15)}} \\ 
\label{proposition:implication28!18} \hypertarget{proposition:implication28!18}{\mbox{(18)}}  \ &  \ \mbox{\qquad}$A\ \land\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!17}{(17)}, \hyperlink{proposition:implication28!13}{(13)}} \\ 
\label{proposition:implication28!19} \hypertarget{proposition:implication28!19}{\mbox{(19)}}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \rightarrow\ ((A\ \land\ B)\ \land\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!11}{(11)}, \hyperlink{proposition:implication28!16}{(16)}} \\ 
\label{proposition:implication28!20} \hypertarget{proposition:implication28!20}{\mbox{(20)}}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \land\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication28!19}{(19)}, \hyperlink{proposition:implication28!18}{(18)}} \\ 
\label{proposition:implication28!21} \hypertarget{proposition:implication28!21}{\mbox{(21)}}  \ &  \ $(A\ \land\ (B\ \land\ C))\ \rightarrow\ ((A\ \land\ B)\ \land\ C)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\section{Propositions about disjunction} \label{chapter4_section5} \hypertarget{chapter4_section5}{}
The disjunction is our theme here.

\begin{prop}
\label{proposition:40} \hypertarget{proposition:40}{}
{\tt \tiny [\verb]proposition:40]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:40!1} \hypertarget{proposition:40!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-1}{axiom~6}} \\ 
\label{proposition:40!2} \hypertarget{proposition:40!2}{\mbox{(2)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:40!1}{(1)}} \\ 
\label{proposition:40!3} \hypertarget{proposition:40!3}{\mbox{(3)}}  \ &  \ $(A\ \lor\ B)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \lor\ B$ in \hyperlink{proposition:40!2}{(2)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:40!4} \hypertarget{proposition:40!4}{\mbox{(4)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:40!5} \hypertarget{proposition:40!5}{\mbox{(5)}}  \ &  \ \mbox{\qquad}$A\ \lor\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!1}{(1)}, \hyperlink{proposition:40!4}{(4)}} \\ 
\label{proposition:40!6} \hypertarget{proposition:40!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}$(A\ \lor\ B)\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!3}{(3)}, \hyperlink{proposition:40!5}{(5)}} \\ 
\label{proposition:40!7} \hypertarget{proposition:40!7}{\mbox{(7)}}  \ &  \ $A\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:40!8} \hypertarget{proposition:40!8}{\mbox{(8)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-2}{axiom~7}} \\ 
\label{proposition:40!9} \hypertarget{proposition:40!9}{\mbox{(9)}}  \ &  \ $C\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:40!8}{(8)}} \\ 
\label{proposition:40!10} \hypertarget{proposition:40!10}{\mbox{(10)}}  \ &  \ $C\ \rightarrow\ (A\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:40!9}{(9)}} \\ 
\label{proposition:40!11} \hypertarget{proposition:40!11}{\mbox{(11)}}  \ &  \ $B\ \rightarrow\ (A\ \lor\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $B$ in \hyperlink{proposition:40!10}{(10)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:40!12} \hypertarget{proposition:40!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:40!13} \hypertarget{proposition:40!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}$A\ \lor\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!11}{(11)}, \hyperlink{proposition:40!12}{(12)}} \\ 
\label{proposition:40!14} \hypertarget{proposition:40!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$(A\ \lor\ B)\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!3}{(3)}, \hyperlink{proposition:40!13}{(13)}} \\ 
\label{proposition:40!15} \hypertarget{proposition:40!15}{\mbox{(15)}}  \ &  \ $B\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:40!16} \hypertarget{proposition:40!16}{\mbox{(16)}}  \ &  \ $C\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A\ \lor\ B$ in \hyperlink{proposition:40!9}{(9)}} \\ 
\label{proposition:40!17} \hypertarget{proposition:40!17}{\mbox{(17)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:40!18} \hypertarget{proposition:40!18}{\mbox{(18)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((B\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:40!17}{(17)}} \\ 
\label{proposition:40!19} \hypertarget{proposition:40!19}{\mbox{(19)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:40!18}{(18)}} \\ 
\label{proposition:40!20} \hypertarget{proposition:40!20}{\mbox{(20)}}  \ &  \ $(B\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:40!19}{(19)}} \\ 
\label{proposition:40!21} \hypertarget{proposition:40!21}{\mbox{(21)}}  \ &  \ $(B\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((C\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(A\ \lor\ B)\ \lor\ C$ in \hyperlink{proposition:40!20}{(20)}} \\ 
\label{proposition:40!22} \hypertarget{proposition:40!22}{\mbox{(22)}}  \ &  \ $(C\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!21}{(21)}, \hyperlink{proposition:40!15}{(15)}} \\ 
\label{proposition:40!23} \hypertarget{proposition:40!23}{\mbox{(23)}}  \ &  \ $(B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!22}{(22)}, \hyperlink{proposition:40!16}{(16)}} \\ 
\label{proposition:40!24} \hypertarget{proposition:40!24}{\mbox{(24)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ (((B\ \lor\ C)\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ (B\ \lor\ C))\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \lor\ C$ in \hyperlink{proposition:40!18}{(18)}} \\ 
\label{proposition:40!25} \hypertarget{proposition:40!25}{\mbox{(25)}}  \ &  \ $(A\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ (((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(A\ \lor\ B)\ \lor\ C$ in \hyperlink{proposition:40!24}{(24)}} \\ 
\label{proposition:40!26} \hypertarget{proposition:40!26}{\mbox{(26)}}  \ &  \ $((B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))\ \rightarrow\ ((A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!25}{(25)}, \hyperlink{proposition:40!7}{(7)}} \\ 
\label{proposition:40!27} \hypertarget{proposition:40!27}{\mbox{(27)}}  \ &  \ $(A\ \lor\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:40!26}{(26)}, \hyperlink{proposition:40!23}{(23)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication41} \hypertarget{proposition:implication41}{}
{\tt \tiny [\verb]proposition:implication41]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication41!1} \hypertarget{proposition:implication41!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-1}{axiom~6}} \\ 
\label{proposition:implication41!2} \hypertarget{proposition:implication41!2}{\mbox{(2)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \lor\ C$ in \hyperlink{proposition:implication41!1}{(1)}} \\ 
\label{proposition:implication41!3} \hypertarget{proposition:implication41!3}{\mbox{(3)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication41!1}{(1)}} \\ 
\label{proposition:implication41!4} \hypertarget{proposition:implication41!4}{\mbox{(4)}}  \ &  \ $B\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication41!3}{(3)}} \\ 
\label{proposition:implication41!5} \hypertarget{proposition:implication41!5}{\mbox{(5)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-2}{axiom~7}} \\ 
\label{proposition:implication41!6} \hypertarget{proposition:implication41!6}{\mbox{(6)}}  \ &  \ $A\ \rightarrow\ (D\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $D$ in \hyperlink{proposition:implication41!5}{(5)}} \\ 
\label{proposition:implication41!7} \hypertarget{proposition:implication41!7}{\mbox{(7)}}  \ &  \ $(B\ \lor\ C)\ \rightarrow\ (D\ \lor\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B\ \lor\ C$ in \hyperlink{proposition:implication41!6}{(6)}} \\ 
\label{proposition:implication41!8} \hypertarget{proposition:implication41!8}{\mbox{(8)}}  \ &  \ $(B\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $A$ in \hyperlink{proposition:implication41!7}{(7)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication41!9} \hypertarget{proposition:implication41!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication41!10} \hypertarget{proposition:implication41!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}$B\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!4}{(4)}, \hyperlink{proposition:implication41!9}{(9)}} \\ 
\label{proposition:implication41!11} \hypertarget{proposition:implication41!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$A\ \lor\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!8}{(8)}, \hyperlink{proposition:implication41!10}{(10)}} \\ 
\label{proposition:implication41!12} \hypertarget{proposition:implication41!12}{\mbox{(12)}}  \ &  \ $B\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication41!13} \hypertarget{proposition:implication41!13}{\mbox{(13)}}  \ &  \ $C\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication41!5}{(5)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication41!14} \hypertarget{proposition:implication41!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$C$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication41!15} \hypertarget{proposition:implication41!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}$B\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!13}{(13)}, \hyperlink{proposition:implication41!14}{(14)}} \\ 
\label{proposition:implication41!16} \hypertarget{proposition:implication41!16}{\mbox{(16)}}  \ &  \ \mbox{\qquad}$A\ \lor\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!8}{(8)}, \hyperlink{proposition:implication41!15}{(15)}} \\ 
\label{proposition:implication41!17} \hypertarget{proposition:implication41!17}{\mbox{(17)}}  \ &  \ $C\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication41!18} \hypertarget{proposition:implication41!18}{\mbox{(18)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication41!19} \hypertarget{proposition:implication41!19}{\mbox{(19)}}  \ &  \ $(A\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((B\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A\ \lor\ (B\ \lor\ C)$ in \hyperlink{proposition:implication41!18}{(18)}} \\ 
\label{proposition:implication41!20} \hypertarget{proposition:implication41!20}{\mbox{(20)}}  \ &  \ $(B\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!19}{(19)}, \hyperlink{proposition:implication41!2}{(2)}} \\ 
\label{proposition:implication41!21} \hypertarget{proposition:implication41!21}{\mbox{(21)}}  \ &  \ $(A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!20}{(20)}, \hyperlink{proposition:implication41!12}{(12)}} \\ 
\label{proposition:implication41!22} \hypertarget{proposition:implication41!22}{\mbox{(22)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((B\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:implication41!18}{(18)}} \\ 
\label{proposition:implication41!23} \hypertarget{proposition:implication41!23}{\mbox{(23)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication41!22}{(22)}} \\ 
\label{proposition:implication41!24} \hypertarget{proposition:implication41!24}{\mbox{(24)}}  \ &  \ $((A\ \lor\ B)\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ (((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \lor\ B$ in \hyperlink{proposition:implication41!23}{(23)}} \\ 
\label{proposition:implication41!25} \hypertarget{proposition:implication41!25}{\mbox{(25)}}  \ &  \ $((A\ \lor\ B)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ ((C\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ (((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $A\ \lor\ (B\ \lor\ C)$ in \hyperlink{proposition:implication41!24}{(24)}} \\ 
\label{proposition:implication41!26} \hypertarget{proposition:implication41!26}{\mbox{(26)}}  \ &  \ $(C\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))\ \rightarrow\ (((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!25}{(25)}, \hyperlink{proposition:implication41!21}{(21)}} \\ 
\label{proposition:implication41!27} \hypertarget{proposition:implication41!27}{\mbox{(27)}}  \ &  \ $((A\ \lor\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication41!26}{(26)}, \hyperlink{proposition:implication41!17}{(17)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication42} \hypertarget{proposition:implication42}{}
{\tt \tiny [\verb]proposition:implication42]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ (B\ \lor\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication42!1} \hypertarget{proposition:implication42!1}{\mbox{(1)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication42!2} \hypertarget{proposition:implication42!2}{\mbox{(2)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((B\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:implication42!1}{(1)}} \\ 
\label{proposition:implication42!3} \hypertarget{proposition:implication42!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication42!2}{(2)}} \\ 
\label{proposition:implication42!4} \hypertarget{proposition:implication42!4}{\mbox{(4)}}  \ &  \ $(A\ \rightarrow\ (B\ \lor\ C))\ \rightarrow\ ((C\ \rightarrow\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ (B\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $B\ \lor\ C$ in \hyperlink{proposition:implication42!3}{(3)}} \\ 
\label{proposition:implication42!5} \hypertarget{proposition:implication42!5}{\mbox{(5)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-1}{axiom~6}} \\ 
\label{proposition:implication42!6} \hypertarget{proposition:implication42!6}{\mbox{(6)}}  \ &  \ $A\ \rightarrow\ (A\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication42!5}{(5)}} \\ 
\label{proposition:implication42!7} \hypertarget{proposition:implication42!7}{\mbox{(7)}}  \ &  \ $B\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication42!6}{(6)}} \\ 
\label{proposition:implication42!8} \hypertarget{proposition:implication42!8}{\mbox{(8)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-2}{axiom~7}} \\ 
\label{proposition:implication42!9} \hypertarget{proposition:implication42!9}{\mbox{(9)}}  \ &  \ $C\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication42!8}{(8)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication42!10} \hypertarget{proposition:implication42!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication42!11} \hypertarget{proposition:implication42!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication42!12} \hypertarget{proposition:implication42!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication42!10}{(10)}, \hyperlink{proposition:implication42!11}{(11)}} \\ 
\label{proposition:implication42!13} \hypertarget{proposition:implication42!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication42!7}{(7)}, \hyperlink{proposition:implication42!12}{(12)}} \\ 
\label{proposition:implication42!14} \hypertarget{proposition:implication42!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication42!15} \hypertarget{proposition:implication42!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}$(C\ \rightarrow\ (B\ \lor\ C))\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication42!4}{(4)}, \hyperlink{proposition:implication42!14}{(14)}} \\ 
\label{proposition:implication42!16} \hypertarget{proposition:implication42!16}{\mbox{(16)}}  \ &  \ \mbox{\qquad}$(A\ \lor\ C)\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication42!15}{(15)}, \hyperlink{proposition:implication42!9}{(9)}} \\ 
\label{proposition:implication42!17} \hypertarget{proposition:implication42!17}{\mbox{(17)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ (B\ \lor\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\section{Propositions about negation} \label{chapter4_section6} \hypertarget{chapter4_section6}{}
Now we look at negation. Here we must use the principle of the excluded middle for the first time.

\begin{prop}
\label{proposition:implication50} \hypertarget{proposition:implication50}{}
{\tt \tiny [\verb]proposition:implication50]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $A\ \rightarrow\ \neg \neg A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication50!1} \hypertarget{proposition:implication50!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{axiom~1}} \\ 
\label{proposition:implication50!2} \hypertarget{proposition:implication50!2}{\mbox{(2)}}  \ &  \ $A\ \rightarrow\ (\neg A\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication50!1}{(1)}} \\ 
\label{proposition:implication50!3} \hypertarget{proposition:implication50!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{axiom~9}} \\ 
\label{proposition:implication50!4} \hypertarget{proposition:implication50!4}{\mbox{(4)}}  \ &  \ $(\neg A\ \rightarrow\ B)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg B)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication50!3}{(3)}} \\ 
\label{proposition:implication50!5} \hypertarget{proposition:implication50!5}{\mbox{(5)}}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication50!4}{(4)}} \\ 
\label{proposition:implication50!6} \hypertarget{proposition:implication50!6}{\mbox{(6)}}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implicationReflexive1}{proposition~1}} \\ 
\label{proposition:implication50!7} \hypertarget{proposition:implication50!7}{\mbox{(7)}}  \ &  \ $\neg A\ \rightarrow\ \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication50!6}{(6)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication50!8} \hypertarget{proposition:implication50!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication50!9} \hypertarget{proposition:implication50!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication50!2}{(2)}, \hyperlink{proposition:implication50!8}{(8)}} \\ 
\label{proposition:implication50!10} \hypertarget{proposition:implication50!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}$(\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication50!5}{(5)}, \hyperlink{proposition:implication50!9}{(9)}} \\ 
\label{proposition:implication50!11} \hypertarget{proposition:implication50!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$\neg \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication50!10}{(10)}, \hyperlink{proposition:implication50!7}{(7)}} \\ 
\label{proposition:implication50!12} \hypertarget{proposition:implication50!12}{\mbox{(12)}}  \ &  \ $A\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication51} \hypertarget{proposition:implication51}{}
{\tt \tiny [\verb]proposition:implication51]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication51!1} \hypertarget{proposition:implication51!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{axiom~1}} \\ 
\label{proposition:implication51!2} \hypertarget{proposition:implication51!2}{\mbox{(2)}}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication51!1}{(1)}} \\ 
\label{proposition:implication51!3} \hypertarget{proposition:implication51!3}{\mbox{(3)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication51!2}{(2)}} \\ 
\label{proposition:implication51!4} \hypertarget{proposition:implication51!4}{\mbox{(4)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $B$ in \hyperlink{proposition:implication51!3}{(3)}} \\ 
\label{proposition:implication51!5} \hypertarget{proposition:implication51!5}{\mbox{(5)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{axiom~9}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication51!6} \hypertarget{proposition:implication51!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ \neg B$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication51!7} \hypertarget{proposition:implication51!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication51!8} \hypertarget{proposition:implication51!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication51!4}{(4)}, \hyperlink{proposition:implication51!7}{(7)}} \\ 
\label{proposition:implication51!9} \hypertarget{proposition:implication51!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$(A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication51!5}{(5)}, \hyperlink{proposition:implication51!8}{(8)}} \\ 
\label{proposition:implication51!10} \hypertarget{proposition:implication51!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$\neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication51!9}{(9)}, \hyperlink{proposition:implication51!6}{(6)}} \\ 
\label{proposition:implication51!11} \hypertarget{proposition:implication51!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ \neg A$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication51!12} \hypertarget{proposition:implication51!12}{\mbox{(12)}}  \ &  \ $(A\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg A)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication52} \hypertarget{proposition:implication52}{}
{\tt \tiny [\verb]proposition:implication52]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication52!1} \hypertarget{proposition:implication52!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:THEN-1}{axiom~1}} \\ 
\label{proposition:implication52!2} \hypertarget{proposition:implication52!2}{\mbox{(2)}}  \ &  \ $C\ \rightarrow\ (B\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication52!1}{(1)}} \\ 
\label{proposition:implication52!3} \hypertarget{proposition:implication52!3}{\mbox{(3)}}  \ &  \ $C\ \rightarrow\ (A\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication52!2}{(2)}} \\ 
\label{proposition:implication52!4} \hypertarget{proposition:implication52!4}{\mbox{(4)}}  \ &  \ $\neg B\ \rightarrow\ (A\ \rightarrow\ \neg B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $\neg B$ in \hyperlink{proposition:implication52!3}{(3)}} \\ 
\label{proposition:implication52!5} \hypertarget{proposition:implication52!5}{\mbox{(5)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{axiom~9}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication52!6} \hypertarget{proposition:implication52!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication52!7} \hypertarget{proposition:implication52!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}$(A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication52!5}{(5)}, \hyperlink{proposition:implication52!6}{(6)}} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication52!8} \hypertarget{proposition:implication52!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$\neg B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication52!9} \hypertarget{proposition:implication52!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A\ \rightarrow\ \neg B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication52!4}{(4)}, \hyperlink{proposition:implication52!8}{(8)}} \\ 
\label{proposition:implication52!10} \hypertarget{proposition:implication52!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$\neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication52!7}{(7)}, \hyperlink{proposition:implication52!9}{(9)}} \\ 
\label{proposition:implication52!11} \hypertarget{proposition:implication52!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$\neg B\ \rightarrow\ \neg A$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication52!12} \hypertarget{proposition:implication52!12}{\mbox{(12)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication54} \hypertarget{proposition:implication54}{}
{\tt \tiny [\verb]proposition:implication54]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg \neg \neg A\ \rightarrow\ \neg A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication54!1} \hypertarget{proposition:implication54!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication50}{proposition~24}} \\ 
\label{proposition:implication54!2} \hypertarget{proposition:implication54!2}{\mbox{(2)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ (\neg B\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication52}{proposition~26}} \\ 
\label{proposition:implication54!3} \hypertarget{proposition:implication54!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ \neg \neg A)\ \rightarrow\ (\neg \neg \neg A\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $\neg \neg A$ in \hyperlink{proposition:implication54!2}{(2)}} \\ 
\label{proposition:implication54!4} \hypertarget{proposition:implication54!4}{\mbox{(4)}}  \ &  \ $\neg \neg \neg A\ \rightarrow\ \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication54!3}{(3)}, \hyperlink{proposition:implication54!1}{(1)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication55} \hypertarget{proposition:implication55}{}
{\tt \tiny [\verb]proposition:implication55]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(\neg A\ \rightarrow\ A)\ \rightarrow\ \neg \neg A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication55!1} \hypertarget{proposition:implication55!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implicationReflexive1}{proposition~1}} \\ 
\label{proposition:implication55!2} \hypertarget{proposition:implication55!2}{\mbox{(2)}}  \ &  \ $\neg A\ \rightarrow\ \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication55!1}{(1)}} \\ 
\label{proposition:implication55!3} \hypertarget{proposition:implication55!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \rightarrow\ \neg B)\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-1}{axiom~9}} \\ 
\label{proposition:implication55!4} \hypertarget{proposition:implication55!4}{\mbox{(4)}}  \ &  \ $(\neg A\ \rightarrow\ B)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg B)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication55!3}{(3)}} \\ 
\label{proposition:implication55!5} \hypertarget{proposition:implication55!5}{\mbox{(5)}}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication55!4}{(4)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication55!6} \hypertarget{proposition:implication55!6}{\mbox{(6)}}  \ &  \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication55!7} \hypertarget{proposition:implication55!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}$(\neg A\ \rightarrow\ \neg A)\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication55!5}{(5)}, \hyperlink{proposition:implication55!6}{(6)}} \\ 
\label{proposition:implication55!8} \hypertarget{proposition:implication55!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}$\neg \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication55!7}{(7)}, \hyperlink{proposition:implication55!2}{(2)}} \\ 
\label{proposition:implication55!9} \hypertarget{proposition:implication55!9}{\mbox{(9)}}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ \neg \neg A$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication56} \hypertarget{proposition:implication56}{}
{\tt \tiny [\verb]proposition:implication56]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $\neg \neg A\ \rightarrow\ A$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication56!1} \hypertarget{proposition:implication56!1}{\mbox{(1)}}  \ &  \ $A\ \lor\ \neg A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-3}{axiom~11}} \\ 
\label{proposition:implication56!2} \hypertarget{proposition:implication56!2}{\mbox{(2)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication56!3} \hypertarget{proposition:implication56!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ A)\ \rightarrow\ ((B\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ A))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $A$ in \hyperlink{proposition:implication56!2}{(2)}} \\ 
\label{proposition:implication56!4} \hypertarget{proposition:implication56!4}{\mbox{(4)}}  \ &  \ $A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implicationReflexive1}{proposition~1}} \\ 
\label{proposition:implication56!5} \hypertarget{proposition:implication56!5}{\mbox{(5)}}  \ &  \ $(B\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!3}{(3)}, \hyperlink{proposition:implication56!4}{(4)}} \\ 
\label{proposition:implication56!6} \hypertarget{proposition:implication56!6}{\mbox{(6)}}  \ &  \ $(\neg A\ \rightarrow\ A)\ \rightarrow\ ((A\ \lor\ \neg A)\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $\neg A$ in \hyperlink{proposition:implication56!5}{(5)}} \\ 
\label{proposition:implication56!7} \hypertarget{proposition:implication56!7}{\mbox{(7)}}  \ &  \ $\neg A\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:NOT-2}{axiom~10}} \\ 
\label{proposition:implication56!8} \hypertarget{proposition:implication56!8}{\mbox{(8)}}  \ &  \ $\neg \neg A\ \rightarrow\ (\neg A\ \rightarrow\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $\neg A$ in \hyperlink{proposition:implication56!7}{(7)}} \\ 
\label{proposition:implication56!9} \hypertarget{proposition:implication56!9}{\mbox{(9)}}  \ &  \ $\neg \neg A\ \rightarrow\ (\neg A\ \rightarrow\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication56!8}{(8)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication56!10} \hypertarget{proposition:implication56!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}$\neg \neg A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication56!11} \hypertarget{proposition:implication56!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}$\neg A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!9}{(9)}, \hyperlink{proposition:implication56!10}{(10)}} \\ 
\label{proposition:implication56!12} \hypertarget{proposition:implication56!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$(A\ \lor\ \neg A)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!6}{(6)}, \hyperlink{proposition:implication56!11}{(11)}} \\ 
\label{proposition:implication56!13} \hypertarget{proposition:implication56!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication56!12}{(12)}, \hyperlink{proposition:implication56!1}{(1)}} \\ 
\label{proposition:implication56!14} \hypertarget{proposition:implication56!14}{\mbox{(14)}}  \ &  \ $\neg \neg A\ \rightarrow\ A$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication57} \hypertarget{proposition:implication57}{}
{\tt \tiny [\verb]proposition:implication57]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $(\neg B\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ B)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication57!1} \hypertarget{proposition:implication57!1}{\mbox{(1)}}  \ &  \ $\neg \neg A\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication56}{proposition~29}} \\ 
\label{proposition:implication57!2} \hypertarget{proposition:implication57!2}{\mbox{(2)}}  \ &  \ $\neg \neg B\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication57!1}{(1)}} \\ 
\label{proposition:implication57!3} \hypertarget{proposition:implication57!3}{\mbox{(3)}}  \ &  \ $(A\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication51}{proposition~25}} \\ 
\label{proposition:implication57!4} \hypertarget{proposition:implication57!4}{\mbox{(4)}}  \ &  \ $(C\ \rightarrow\ \neg B)\ \rightarrow\ (B\ \rightarrow\ \neg C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication57!3}{(3)}} \\ 
\label{proposition:implication57!5} \hypertarget{proposition:implication57!5}{\mbox{(5)}}  \ &  \ $(C\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ \neg C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A$ in \hyperlink{proposition:implication57!4}{(4)}} \\ 
\label{proposition:implication57!6} \hypertarget{proposition:implication57!6}{\mbox{(6)}}  \ &  \ $(\neg B\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ \neg \neg B)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $\neg B$ in \hyperlink{proposition:implication57!5}{(5)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication57!7} \hypertarget{proposition:implication57!7}{\mbox{(7)}}  \ &  \ \mbox{\qquad}$\neg B\ \rightarrow\ \neg A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication57!8} \hypertarget{proposition:implication57!8}{\mbox{(8)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ \neg \neg B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication57!6}{(6)}, \hyperlink{proposition:implication57!7}{(7)}} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication57!9} \hypertarget{proposition:implication57!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication57!10} \hypertarget{proposition:implication57!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$\neg \neg B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication57!8}{(8)}, \hyperlink{proposition:implication57!9}{(9)}} \\ 
\label{proposition:implication57!11} \hypertarget{proposition:implication57!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication57!2}{(2)}, \hyperlink{proposition:implication57!10}{(10)}} \\ 
\label{proposition:implication57!12} \hypertarget{proposition:implication57!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$A\ \rightarrow\ B$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication57!13} \hypertarget{proposition:implication57!13}{\mbox{(13)}}  \ &  \ $(\neg B\ \rightarrow\ \neg A)\ \rightarrow\ (A\ \rightarrow\ B)$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\section{Mixing conjunction and disjunction.} \label{chapter4_section7} \hypertarget{chapter4_section7}{}
Now we show how disjunction and conjunction are connected.

\begin{prop}
\label{proposition:implication70} \hypertarget{proposition:implication70}{}
{\tt \tiny [\verb]proposition:implication70]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \rightarrow\ C)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication70!1} \hypertarget{proposition:implication70!1}{\mbox{(1)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication20}{proposition~15}} \\ 
\label{proposition:implication70!2} \hypertarget{proposition:implication70!2}{\mbox{(2)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ D))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:implication70!1}{(1)}} \\ 
\label{proposition:implication70!3} \hypertarget{proposition:implication70!3}{\mbox{(3)}}  \ &  \ $((A\ \rightarrow\ C)\ \rightarrow\ (B\ \rightarrow\ D))\ \rightarrow\ (((A\ \rightarrow\ C)\ \land\ B)\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \rightarrow\ C$ in \hyperlink{proposition:implication70!2}{(2)}} \\ 
\label{proposition:implication70!4} \hypertarget{proposition:implication70!4}{\mbox{(4)}}  \ &  \ $((A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ D))\ \rightarrow\ (((A\ \rightarrow\ C)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \rightarrow\ C$ in \hyperlink{proposition:implication70!3}{(3)}} \\ 
\label{proposition:implication70!5} \hypertarget{proposition:implication70!5}{\mbox{(5)}}  \ &  \ $((A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C)))\ \rightarrow\ (((A\ \rightarrow\ C)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(A\ \lor\ B)\ \rightarrow\ C$ in \hyperlink{proposition:implication70!4}{(4)}} \\ 
\label{proposition:implication70!6} \hypertarget{proposition:implication70!6}{\mbox{(6)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication70!7} \hypertarget{proposition:implication70!7}{\mbox{(7)}}  \ &  \ $((A\ \rightarrow\ C)\ \land\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication70!5}{(5)}, \hyperlink{proposition:implication70!6}{(6)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication71} \hypertarget{proposition:implication71}{}
{\tt \tiny [\verb]proposition:implication71]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \land\ B)\ \lor\ C)\ \rightarrow\ ((A\ \lor\ C)\ \land\ (B\ \lor\ C))$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication71!1} \hypertarget{proposition:implication71!1}{\mbox{(1)}}  \ &  \ $B\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-3}{axiom~5}} \\ 
\label{proposition:implication71!2} \hypertarget{proposition:implication71!2}{\mbox{(2)}}  \ &  \ $(B\ \lor\ C)\ \rightarrow\ (A\ \rightarrow\ (A\ \land\ (B\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \lor\ C$ in \hyperlink{proposition:implication71!1}{(1)}} \\ 
\label{proposition:implication71!3} \hypertarget{proposition:implication71!3}{\mbox{(3)}}  \ &  \ $(B\ \lor\ C)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ ((A\ \lor\ C)\ \land\ (B\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \lor\ C$ in \hyperlink{proposition:implication71!2}{(2)}} \\ 
\label{proposition:implication71!4} \hypertarget{proposition:implication71!4}{\mbox{(4)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ A$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-1}{axiom~3}} \\ 
\label{proposition:implication71!5} \hypertarget{proposition:implication71!5}{\mbox{(5)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication42}{proposition~23}} \\ 
\label{proposition:implication71!6} \hypertarget{proposition:implication71!6}{\mbox{(6)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ (D\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $D$ in \hyperlink{proposition:implication71!5}{(5)}} \\ 
\label{proposition:implication71!7} \hypertarget{proposition:implication71!7}{\mbox{(7)}}  \ &  \ $((A\ \land\ B)\ \rightarrow\ D)\ \rightarrow\ (((A\ \land\ B)\ \lor\ C)\ \rightarrow\ (D\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \land\ B$ in \hyperlink{proposition:implication71!6}{(6)}} \\ 
\label{proposition:implication71!8} \hypertarget{proposition:implication71!8}{\mbox{(8)}}  \ &  \ $((A\ \land\ B)\ \rightarrow\ A)\ \rightarrow\ (((A\ \land\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $A$ in \hyperlink{proposition:implication71!7}{(7)}} \\ 
\label{proposition:implication71!9} \hypertarget{proposition:implication71!9}{\mbox{(9)}}  \ &  \ $((A\ \land\ B)\ \lor\ C)\ \rightarrow\ (A\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication71!8}{(8)}, \hyperlink{proposition:implication71!4}{(4)}} \\ 
\label{proposition:implication71!10} \hypertarget{proposition:implication71!10}{\mbox{(10)}}  \ &  \ $(A\ \land\ B)\ \rightarrow\ B$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:AND-2}{axiom~4}} \\ 
\label{proposition:implication71!11} \hypertarget{proposition:implication71!11}{\mbox{(11)}}  \ &  \ $((A\ \land\ B)\ \rightarrow\ B)\ \rightarrow\ (((A\ \land\ B)\ \lor\ C)\ \rightarrow\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $B$ in \hyperlink{proposition:implication71!7}{(7)}} \\ 
\label{proposition:implication71!12} \hypertarget{proposition:implication71!12}{\mbox{(12)}}  \ &  \ $((A\ \land\ B)\ \lor\ C)\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication71!11}{(11)}, \hyperlink{proposition:implication71!10}{(10)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication71!13} \hypertarget{proposition:implication71!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}$(A\ \land\ B)\ \lor\ C$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication71!14} \hypertarget{proposition:implication71!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$A\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication71!9}{(9)}, \hyperlink{proposition:implication71!13}{(13)}} \\ 
\label{proposition:implication71!15} \hypertarget{proposition:implication71!15}{\mbox{(15)}}  \ &  \ \mbox{\qquad}$B\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication71!12}{(12)}, \hyperlink{proposition:implication71!13}{(13)}} \\ 
\label{proposition:implication71!16} \hypertarget{proposition:implication71!16}{\mbox{(16)}}  \ &  \ \mbox{\qquad}$(A\ \lor\ C)\ \rightarrow\ ((A\ \lor\ C)\ \land\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication71!3}{(3)}, \hyperlink{proposition:implication71!15}{(15)}} \\ 
\label{proposition:implication71!17} \hypertarget{proposition:implication71!17}{\mbox{(17)}}  \ &  \ \mbox{\qquad}$(A\ \lor\ C)\ \land\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication71!16}{(16)}, \hyperlink{proposition:implication71!14}{(14)}} \\ 
\label{proposition:implication71!18} \hypertarget{proposition:implication71!18}{\mbox{(18)}}  \ &  \ $((A\ \land\ B)\ \lor\ C)\ \rightarrow\ ((A\ \lor\ C)\ \land\ (B\ \lor\ C))$ \ &  \ {\tiny Conclusion} \\ 
 & & \qedhere
\end{longtable}
\end{proof}


\begin{prop}
\label{proposition:implication72} \hypertarget{proposition:implication72}{}
{\tt \tiny [\verb]proposition:implication72]]}
\mbox{}
\begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}}
\centering $((A\ \lor\ C)\ \land\ (B\ \lor\ C))\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)$
\end{longtable}

\end{prop}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{proposition:implication72!1} \hypertarget{proposition:implication72!1}{\mbox{(1)}}  \ &  \ $A\ \rightarrow\ (B\ \lor\ A)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-2}{axiom~7}} \\ 
\label{proposition:implication72!2} \hypertarget{proposition:implication72!2}{\mbox{(2)}}  \ &  \ $C\ \rightarrow\ (B\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $C$ in \hyperlink{proposition:implication72!1}{(1)}} \\ 
\label{proposition:implication72!3} \hypertarget{proposition:implication72!3}{\mbox{(3)}}  \ &  \ $C\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A\ \land\ B$ in \hyperlink{proposition:implication72!2}{(2)}} \\ 
\label{proposition:implication72!4} \hypertarget{proposition:implication72!4}{\mbox{(4)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication72!5} \hypertarget{proposition:implication72!5}{\mbox{(5)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((B\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:implication72!4}{(4)}} \\ 
\label{proposition:implication72!6} \hypertarget{proposition:implication72!6}{\mbox{(6)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication72!5}{(5)}} \\ 
\label{proposition:implication72!7} \hypertarget{proposition:implication72!7}{\mbox{(7)}}  \ &  \ $(B\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $B$ in \hyperlink{proposition:implication72!6}{(6)}} \\ 
\label{proposition:implication72!8} \hypertarget{proposition:implication72!8}{\mbox{(8)}}  \ &  \ $(B\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))\ \rightarrow\ ((C\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(A\ \land\ B)\ \lor\ C$ in \hyperlink{proposition:implication72!7}{(7)}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication72!9} \hypertarget{proposition:implication72!9}{\mbox{(9)}}  \ &  \ \mbox{\qquad}$C$ \ &  \ {\tiny Hypothesis} \\ 
 \ &  \ \mbox{\qquad}Conditional Proof
 \ &  \  \\ 
\label{proposition:implication72!10} \hypertarget{proposition:implication72!10}{\mbox{(10)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$B$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication72!11} \hypertarget{proposition:implication72!11}{\mbox{(11)}}  \ &  \ \mbox{\qquad}\mbox{\qquad}$(A\ \land\ B)\ \lor\ C$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!3}{(3)}, \hyperlink{proposition:implication72!9}{(9)}} \\ 
\label{proposition:implication72!12} \hypertarget{proposition:implication72!12}{\mbox{(12)}}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication72!13} \hypertarget{proposition:implication72!13}{\mbox{(13)}}  \ &  \ \mbox{\qquad}$(C\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!8}{(8)}, \hyperlink{proposition:implication72!12}{(12)}} \\ 
\label{proposition:implication72!14} \hypertarget{proposition:implication72!14}{\mbox{(14)}}  \ &  \ \mbox{\qquad}$(B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!13}{(13)}, \hyperlink{proposition:implication72!3}{(3)}} \\ 
\label{proposition:implication72!15} \hypertarget{proposition:implication72!15}{\mbox{(15)}}  \ &  \ $C\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication72!16} \hypertarget{proposition:implication72!16}{\mbox{(16)}}  \ &  \ $(A\ \rightarrow\ B)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication42}{proposition~23}} \\ 
\label{proposition:implication72!17} \hypertarget{proposition:implication72!17}{\mbox{(17)}}  \ &  \ $(D\ \rightarrow\ B)\ \rightarrow\ ((D\ \lor\ C)\ \rightarrow\ (B\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $D$ in \hyperlink{proposition:implication72!16}{(16)}} \\ 
\label{proposition:implication72!18} \hypertarget{proposition:implication72!18}{\mbox{(18)}}  \ &  \ $(D\ \rightarrow\ (A\ \land\ B))\ \rightarrow\ ((D\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $A\ \land\ B$ in \hyperlink{proposition:implication72!17}{(17)}} \\ 
\label{proposition:implication72!19} \hypertarget{proposition:implication72!19}{\mbox{(19)}}  \ &  \ $(B\ \rightarrow\ (A\ \land\ B))\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $B$ in \hyperlink{proposition:implication72!18}{(18)}} \\ 
\label{proposition:implication72!20} \hypertarget{proposition:implication72!20}{\mbox{(20)}}  \ &  \ $A\ \rightarrow\ (B\ \rightarrow\ (A\ \land\ B))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:AND-3b}{proposition~10}} \\ 
 \ &  \ Conditional Proof
 \ &  \  \\ 
\label{proposition:implication72!21} \hypertarget{proposition:implication72!21}{\mbox{(21)}}  \ &  \ \mbox{\qquad}$A$ \ &  \ {\tiny Hypothesis} \\ 
\label{proposition:implication72!22} \hypertarget{proposition:implication72!22}{\mbox{(22)}}  \ &  \ \mbox{\qquad}$B\ \rightarrow\ (A\ \land\ B)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!20}{(20)}, \hyperlink{proposition:implication72!21}{(21)}} \\ 
\label{proposition:implication72!23} \hypertarget{proposition:implication72!23}{\mbox{(23)}}  \ &  \ \mbox{\qquad}$(B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!19}{(19)}, \hyperlink{proposition:implication72!22}{(22)}} \\ 
\label{proposition:implication72!24} \hypertarget{proposition:implication72!24}{\mbox{(24)}}  \ &  \ $A\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))$ \ &  \ {\tiny Conclusion} \\ 
\label{proposition:implication72!25} \hypertarget{proposition:implication72!25}{\mbox{(25)}}  \ &  \ $(A\ \rightarrow\ C)\ \rightarrow\ ((B\ \rightarrow\ C)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{axiom:OR-3}{axiom~8}} \\ 
\label{proposition:implication72!26} \hypertarget{proposition:implication72!26}{\mbox{(26)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((B\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ B)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:implication72!25}{(25)}} \\ 
\label{proposition:implication72!27} \hypertarget{proposition:implication72!27}{\mbox{(27)}}  \ &  \ $(A\ \rightarrow\ D)\ \rightarrow\ ((C\ \rightarrow\ D)\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ D))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $C$ in \hyperlink{proposition:implication72!26}{(26)}} \\ 
\label{proposition:implication72!28} \hypertarget{proposition:implication72!28}{\mbox{(28)}}  \ &  \ $(A\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)))\ \rightarrow\ ((C\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)))\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)$ in \hyperlink{proposition:implication72!27}{(27)}} \\ 
\label{proposition:implication72!29} \hypertarget{proposition:implication72!29}{\mbox{(29)}}  \ &  \ $(C\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)))\ \rightarrow\ ((A\ \lor\ C)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!28}{(28)}, \hyperlink{proposition:implication72!24}{(24)}} \\ 
\label{proposition:implication72!30} \hypertarget{proposition:implication72!30}{\mbox{(30)}}  \ &  \ $(A\ \lor\ C)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!29}{(29)}, \hyperlink{proposition:implication72!15}{(15)}} \\ 
\label{proposition:implication72!31} \hypertarget{proposition:implication72!31}{\mbox{(31)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ C))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!Add}{Add} \hyperlink{proposition:implication20}{proposition~15}} \\ 
\label{proposition:implication72!32} \hypertarget{proposition:implication72!32}{\mbox{(32)}}  \ &  \ $(A\ \rightarrow\ (B\ \rightarrow\ D))\ \rightarrow\ ((A\ \land\ B)\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $C$ by $D$ in \hyperlink{proposition:implication72!31}{(31)}} \\ 
\label{proposition:implication72!33} \hypertarget{proposition:implication72!33}{\mbox{(33)}}  \ &  \ $((A\ \lor\ C)\ \rightarrow\ (B\ \rightarrow\ D))\ \rightarrow\ (((A\ \lor\ C)\ \land\ B)\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $A$ by $A\ \lor\ C$ in \hyperlink{proposition:implication72!32}{(32)}} \\ 
\label{proposition:implication72!34} \hypertarget{proposition:implication72!34}{\mbox{(34)}}  \ &  \ $((A\ \lor\ C)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ D))\ \rightarrow\ (((A\ \lor\ C)\ \land\ (B\ \lor\ C))\ \rightarrow\ D)$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $B$ by $B\ \lor\ C$ in \hyperlink{proposition:implication72!33}{(33)}} \\ 
\label{proposition:implication72!35} \hypertarget{proposition:implication72!35}{\mbox{(35)}}  \ &  \ $((A\ \lor\ C)\ \rightarrow\ ((B\ \lor\ C)\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)))\ \rightarrow\ (((A\ \lor\ C)\ \land\ (B\ \lor\ C))\ \rightarrow\ ((A\ \land\ B)\ \lor\ C))$ \ &  \ {\tiny \hyperlink{rule:CP!SubstPred}{SubstPred} $D$ by $(A\ \land\ B)\ \lor\ C$ in \hyperlink{proposition:implication72!34}{(34)}} \\ 
\label{proposition:implication72!36} \hypertarget{proposition:implication72!36}{\mbox{(36)}}  \ &  \ $((A\ \lor\ C)\ \land\ (B\ \lor\ C))\ \rightarrow\ ((A\ \land\ B)\ \lor\ C)$ \ &  \ {\tiny \hyperlink{rule:CP!MP}{MP} \hyperlink{proposition:implication72!35}{(35)}, \hyperlink{proposition:implication72!30}{(30)}} \\ 
 & & \qedhere
\end{longtable}
\end{proof}



%% end of chapter Propositional Calculus

\backmatter

\begin{thebibliography}{99}
\addcontentsline{toc}{chapter}{Bibliography}
\bibitem{novikov} \emph{P.S. Novikov}, Elements of Mathematical Logic, Edinburgh: Oliver and Boyd, 1964.

\bibitem{detnieks} \emph{V.~Detlovs, K.~Podnieks}, Introduction to Mathematical Logic, 
           \url{http://www.ltn.lv/~podnieks/mlog/ml.htm}.

\bibitem{hilback} \emph{D.~Hilbert, W.~Ackermann}, Grundz{\"u}ge der theoretischen Logik, 2nd ed., Berlin: Springer, 1938. English version: Principles of Mathematical Logic, Chelsea, New York 1950, ed. by R.~E.~Luce.
           See also \url{http://www.math.uwaterloo.ca/~snburris/htdocs/scav/hilbert/hilbert.html}

\bibitem{mendelson} \emph{E.~Mendelson}, Introduction to Mathematical Logic, 3rd. ed., Belmont, CA: Wadsworth, 1987.



%% QEDEQ modules that use this one:
\bibitem{qedeq_logic_v1} qedeq\_logic\_v1 \url{http://www.qedeq.org/0_04_05/doc/math/qedeq_logic_v1.xml}


\end{thebibliography}
\addcontentsline{toc}{chapter}{\indexname} \printindex

\end{document}