%%% ====================================================================
%%% @LaTeX-file generated by com.meyling.principia.latex.Module2Latex
%%% ====================================================================

\documentclass{amsart}

\usepackage{amsmath,amsthm,amsfonts}
\usepackage[]{color}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{varioref}
\usepackage[a4paper,bookmarksnumbered,colorlinks,breaklinks,plainpages,backref,bookmarksopen=true,pdfpagemode=None]{hyperref}

\oddsidemargin       8mm
\evensidemargin      9mm
\topmargin           0mm
\headsep             10mm
\marginparsep        2.5mm
\marginparwidth      25mm
\textwidth           160mm
\textheight          220mm

\makeatletter
\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn\fi
\chapter*{List of Figures}
{\let\\ \ \markboth{Title}{List of Figures}}
\addcontentsline{toc}{chapter}{\protect
\numberline{LIST OF FIGURES\string\hss}}
\@starttoc{lof}\if@restonecol \twocolumn\fi}
\makeatother
\def\boldindex#1{\textbf{\hyperpage{#1}}}

\newtheorem{axm}{Axiom}[section]
\newtheorem{abr}{Abbreviation}[section]
\newtheorem{thm}{Theorem}[section]
\newtheorem{dec}{Rule Declaration}[section]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{prop}{Proposition}
\newtheorem{lem}[thm]{Lemma}
\theoremstyle{remark}
\newtheorem*{rmk}{Remark}

\makeindex
\makeatletter
\externaldocument{prophilbert1_1.00.00_1.00.00.qedeq}
\hyperbaseurl{prophilbert1_1.00.00_1.00.00.qedeq}
\makeatother

\setlength{\LTleft}{0pt}
\setlength{\LTright}{0pt}

\sloppy

\begin{document}

\title{First theorems of Propositional Calculus}
\author{Michael Meyling}
\email{principa@meyling.com}
\date{2002-07-27T20:51:19}

\begin{abstract}
This module includes first proofs of propositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)
\end{abstract}

\makeatletter
\long\def\hyper@section@backref#1#2#3{%
\typeout{BACK REF #1 / #2 / #3}%
\hyperlink{#3}{#2}}
\makeatother
\pdfbookmark{Title}{tit}
\setlongtables
\maketitle
\tableofcontents


\section*{module specification}

Author of this module: 
\begin{longtable}[h!]{l@{\extracolsep{\fill}}l}
Michael Meyling & michael@meyling.com \\
\end{longtable}


\medskip
This module has the following specification:

\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & prophilbert1 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{http://www.meyling.com/principia/0_00_51/prophilbert1_1.00.00_1.00.00.qedeq} \\
\end{longtable}


\medskip
The following modules were used:

\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & propaxiom \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{propaxiom_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{propaxiom_1.00.00_1.00.00.pdf}  \\
\end{longtable}

\medskip
Is used by the following modules:

\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & prophilbert2 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{prophilbert2_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{prophilbert2_1.00.00_1.00.00.pdf}  \\
\end{longtable}



First we prove a simple implication, that follows directly from the fourth axiom:




\begin{thm}
\hypertarget{hilb1}{}
\begin{displaymath}
((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb1:1}
  $1$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{hilb1:2}
  $2$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((\neg A\ \vee \  P)\ \Rightarrow \  (\neg A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg A$ in \hyperref[hilb1:1]{$1$}
} \\
\label{hilb1:3}
  $3$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (\neg A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb1:2]{$2$} at occurence $1$
} \\
\label{hilb1:4}
  $4$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb1:3]{$3$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}


This proposition is the form for the Hypothetical Syllogism.



\bigskip




The self implication could be derived:




\begin{thm}
\hypertarget{hilb2}{}
\begin{displaymath}
(P\ \Rightarrow \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb2:1}
  $1$ & $(P\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb2:2}
  $2$ & $(P\ \Rightarrow \  (P\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[hilb2:1]{$1$}
} \\
\label{hilb2:3}
  $3$ & $((P\ \vee \  P)\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
\label{hilb2:4}
  $4$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb1}{hilb1} } \\
\label{hilb2:5}
  $5$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb2:4]{$4$}
} \\
\label{hilb2:6}
  $6$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb2:5]{$5$}
} \\
\label{hilb2:7}
  $7$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb2:6]{$6$}
} \\
\label{hilb2:8}
  $8$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \Rightarrow \  D)\ \Rightarrow \  (P\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb2:7]{$7$}
} \\
\label{hilb2:9}
  $9$ & $((D\ \Rightarrow \  P)\ \Rightarrow \  ((P\ \Rightarrow \  D)\ \Rightarrow \  (P\ \Rightarrow \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $P$ in \hyperref[hilb2:8]{$8$}
} \\
\label{hilb2:10}
  $10$ & $(((P\ \vee \  P)\ \Rightarrow \  P)\ \Rightarrow \  ((P\ \Rightarrow \  (P\ \vee \  P))\ \Rightarrow \  (P\ \Rightarrow \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  P)$ in \hyperref[hilb2:9]{$9$}
} \\
\label{hilb2:11}
  $11$ & $((P\ \Rightarrow \  (P\ \vee \  P))\ \Rightarrow \  (P\ \Rightarrow \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb2:3]{$3$}, \hyperref[hilb2:10]{$10$}} \\
\label{hilb2:12}
  $12$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb2:2]{$2$}, \hyperref[hilb2:11]{$11$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



One form of the classical `tertium non datur'




\begin{thm}
\hypertarget{hilb3}{}
\begin{displaymath}
(\neg P\ \vee \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb3:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{hilb3:2}
  $2$ & $(\neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb3:1]{$1$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



The standard form of the excluded middle:




\begin{thm}
\hypertarget{hilb4}{}
\begin{displaymath}
(P\ \vee \  \neg P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb4:1}
  $1$ & $(\neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb3}{hilb3} } \\
\label{hilb4:2}
  $2$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{hilb4:3}
  $3$ & $((P\ \vee \  A)\ \Rightarrow \  (A\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb4:2]{$2$}
} \\
\label{hilb4:4}
  $4$ & $((B\ \vee \  A)\ \Rightarrow \  (A\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb4:3]{$3$}
} \\
\label{hilb4:5}
  $5$ & $((B\ \vee \  P)\ \Rightarrow \  (P\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P$ in \hyperref[hilb4:4]{$4$}
} \\
\label{hilb4:6}
  $6$ & $((\neg P\ \vee \  P)\ \Rightarrow \  (P\ \vee \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg P$ in \hyperref[hilb4:5]{$5$}
} \\
\label{hilb4:7}
  $7$ & $(P\ \vee \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb4:1]{$1$}, \hyperref[hilb4:6]{$6$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Double negation is implicated:




\begin{thm}
\hypertarget{hilb5}{}
\begin{displaymath}
(P\ \Rightarrow \  \neg \neg P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb5:1}
  $1$ & $(P\ \vee \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb4}{hilb4} } \\
\label{hilb5:2}
  $2$ & $(\neg P\ \vee \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P$ in \hyperref[hilb5:1]{$1$}
} \\
\label{hilb5:3}
  $3$ & $(P\ \Rightarrow \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb5:2]{$2$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



The reverse is also true:




\begin{thm}
\hypertarget{hilb6}{}
\begin{displaymath}
(\neg \neg P\ \Rightarrow \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb6:1}
  $1$ & $(P\ \Rightarrow \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb5}{hilb5} } \\
\label{hilb6:2}
  $2$ & $(\neg P\ \Rightarrow \  \neg \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P$ in \hyperref[hilb6:1]{$1$}
} \\
\label{hilb6:3}
  $3$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{hilb6:4}
  $4$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb6:3]{$3$}
} \\
\label{hilb6:5}
  $5$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb6:4]{$4$}
} \\
\label{hilb6:6}
  $6$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  D)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb6:5]{$5$}
} \\
\label{hilb6:7}
  $7$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb6:6]{$6$}
} \\
\label{hilb6:8}
  $8$ & $((D\ \Rightarrow \  \neg \neg \neg P)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  \neg \neg \neg P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg \neg \neg P$ in \hyperref[hilb6:7]{$7$}
} \\
\label{hilb6:9}
  $9$ & $((\neg P\ \Rightarrow \  \neg \neg \neg P)\ \Rightarrow \  ((P\ \vee \  \neg P)\ \Rightarrow \  (P\ \vee \  \neg \neg \neg P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $\neg P$ in \hyperref[hilb6:8]{$8$}
} \\
\label{hilb6:10}
  $10$ & $((P\ \vee \  \neg P)\ \Rightarrow \  (P\ \vee \  \neg \neg \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb6:2]{$2$}, \hyperref[hilb6:9]{$9$}} \\
\label{hilb6:11}
  $11$ & $(P\ \vee \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb4}{hilb4} } \\
\label{hilb6:12}
  $12$ & $(P\ \vee \  \neg \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb6:11]{$11$}, \hyperref[hilb6:10]{$10$}} \\
\label{hilb6:13}
  $13$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{hilb6:14}
  $14$ & $((P\ \vee \  A)\ \Rightarrow \  (A\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb6:13]{$13$}
} \\
\label{hilb6:15}
  $15$ & $((B\ \vee \  A)\ \Rightarrow \  (A\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb6:14]{$14$}
} \\
\label{hilb6:16}
  $16$ & $((B\ \vee \  \neg \neg \neg P)\ \Rightarrow \  (\neg \neg \neg P\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg \neg \neg P$ in \hyperref[hilb6:15]{$15$}
} \\
\label{hilb6:17}
  $17$ & $((P\ \vee \  \neg \neg \neg P)\ \Rightarrow \  (\neg \neg \neg P\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb6:16]{$16$}
} \\
\label{hilb6:18}
  $18$ & $(\neg \neg \neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb6:12]{$12$}, \hyperref[hilb6:17]{$17$}} \\
\label{hilb6:19}
  $19$ & $(\neg \neg P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb6:18]{$18$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



The correct reverse of an implication:




\begin{thm}
\hypertarget{hilb7}{}
\begin{displaymath}
((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg Q\ \Rightarrow \  \neg P))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb7:1}
  $1$ & $(P\ \Rightarrow \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb5}{hilb5} } \\
\label{hilb7:2}
  $2$ & $(Q\ \Rightarrow \  \neg \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb7:1]{$1$}
} \\
\label{hilb7:3}
  $3$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{hilb7:4}
  $4$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb7:3]{$3$}
} \\
\label{hilb7:5}
  $5$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb7:4]{$4$}
} \\
\label{hilb7:6}
  $6$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  D)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb7:5]{$5$}
} \\
\label{hilb7:7}
  $7$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((\neg P\ \vee \  D)\ \Rightarrow \  (\neg P\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg P$ in \hyperref[hilb7:6]{$6$}
} \\
\label{hilb7:8}
  $8$ & $((D\ \Rightarrow \  \neg \neg Q)\ \Rightarrow \  ((\neg P\ \vee \  D)\ \Rightarrow \  (\neg P\ \vee \  \neg \neg Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg \neg Q$ in \hyperref[hilb7:7]{$7$}
} \\
\label{hilb7:9}
  $9$ & $((Q\ \Rightarrow \  \neg \neg Q)\ \Rightarrow \  ((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg P\ \vee \  \neg \neg Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $Q$ in \hyperref[hilb7:8]{$8$}
} \\
\label{hilb7:10}
  $10$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg P\ \vee \  \neg \neg Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb7:2]{$2$}, \hyperref[hilb7:9]{$9$}} \\
\label{hilb7:11}
  $11$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{hilb7:12}
  $12$ & $((P\ \vee \  A)\ \Rightarrow \  (A\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb7:11]{$11$}
} \\
\label{hilb7:13}
  $13$ & $((B\ \vee \  A)\ \Rightarrow \  (A\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb7:12]{$12$}
} \\
\label{hilb7:14}
  $14$ & $((B\ \vee \  \neg \neg Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg \neg Q$ in \hyperref[hilb7:13]{$13$}
} \\
\label{hilb7:15}
  $15$ & $((\neg P\ \vee \  \neg \neg Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg P$ in \hyperref[hilb7:14]{$14$}
} \\
\label{hilb7:16}
  $16$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb1}{hilb1} } \\
\label{hilb7:17}
  $17$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb7:16]{$16$}
} \\
\label{hilb7:18}
  $18$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb7:17]{$17$}
} \\
\label{hilb7:19}
  $19$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb7:18]{$18$}
} \\
\label{hilb7:20}
  $20$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((\neg P\ \vee \  Q)\ \Rightarrow \  D)\ \Rightarrow \  ((\neg P\ \vee \  Q)\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(\neg P\ \vee \  Q)$ in \hyperref[hilb7:19]{$19$}
} \\
\label{hilb7:21}
  $21$ & $((D\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))\ \Rightarrow \  (((\neg P\ \vee \  Q)\ \Rightarrow \  D)\ \Rightarrow \  ((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg \neg Q\ \vee \  \neg P)$ in \hyperref[hilb7:20]{$20$}
} \\
\label{hilb7:22}
  $22$ & $(((\neg P\ \vee \  \neg \neg Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))\ \Rightarrow \  (((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg P\ \vee \  \neg \neg Q))\ \Rightarrow \  ((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg P\ \vee \  \neg \neg Q)$ in \hyperref[hilb7:21]{$21$}
} \\
\label{hilb7:23}
  $23$ & $(((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg P\ \vee \  \neg \neg Q))\ \Rightarrow \  ((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb7:15]{$15$}, \hyperref[hilb7:22]{$22$}} \\
\label{hilb7:24}
  $24$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb7:10]{$10$}, \hyperref[hilb7:23]{$23$}} \\
\label{hilb7:25}
  $25$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb7:24]{$24$} at occurence $1$
} \\
\label{hilb7:26}
  $26$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg Q\ \Rightarrow \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb7:25]{$25$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Definition of an Implication 1. part:




\begin{thm}
\hypertarget{defimpl1}{}
\begin{displaymath}
((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg P\ \vee \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defimpl1:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defimpl1:2}
  $2$ & $(A\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[defimpl1:1]{$1$}
} \\
\label{defimpl1:3}
  $3$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (P\ \Rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \Rightarrow \  Q)$ in \hyperref[defimpl1:2]{$2$}
} \\
\label{defimpl1:4}
  $4$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[defimpl1:3]{$3$} at occurence $3$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Definition of an Implication 2. part:




\begin{thm}
\hypertarget{defimpl2}{}
\begin{displaymath}
((\neg P\ \vee \  Q)\ \Rightarrow \  (P\ \Rightarrow \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defimpl2:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defimpl2:2}
  $2$ & $(A\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[defimpl2:1]{$1$}
} \\
\label{defimpl2:3}
  $3$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (P\ \Rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \Rightarrow \  Q)$ in \hyperref[defimpl2:2]{$2$}
} \\
\label{defimpl2:4}
  $4$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (P\ \Rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[defimpl2:3]{$3$} at occurence $2$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Definition of a Conjunction 1. part:




\begin{thm}
\hypertarget{defand1}{}
\begin{displaymath}
((P\ \wedge \  Q)\ \Rightarrow \  \neg (\neg P\ \vee \  \neg Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defand1:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defand1:2}
  $2$ & $(A\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[defand1:1]{$1$}
} \\
\label{defand1:3}
  $3$ & $((P\ \wedge \  Q)\ \Rightarrow \  (P\ \wedge \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \wedge \  Q)$ in \hyperref[defand1:2]{$2$}
} \\
\label{defand1:4}
  $4$ & $((P\ \wedge \  Q)\ \Rightarrow \  \neg (\neg P\ \vee \  \neg Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[defand1:3]{$3$} at occurence $2$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Definition of a Conjunction 2. part:




\begin{thm}
\hypertarget{defand2}{}
\begin{displaymath}
(\neg (\neg P\ \vee \  \neg Q)\ \Rightarrow \  (P\ \wedge \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defand2:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defand2:2}
  $2$ & $(A\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[defand2:1]{$1$}
} \\
\label{defand2:3}
  $3$ & $((P\ \wedge \  Q)\ \Rightarrow \  (P\ \wedge \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \wedge \  Q)$ in \hyperref[defand2:2]{$2$}
} \\
\label{defand2:4}
  $4$ & $(\neg (\neg P\ \vee \  \neg Q)\ \Rightarrow \  (P\ \wedge \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[defand2:3]{$3$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Definition of an Equivalence 1. part:




\begin{thm}
\hypertarget{defequi1}{}
\begin{displaymath}
((P\ \Leftrightarrow \  Q)\ \Rightarrow \  ((P\ \Rightarrow \  Q)\ \wedge \  (Q\ \Rightarrow \  P)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defequi1:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defequi1:2}
  $2$ & $(A\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[defequi1:1]{$1$}
} \\
\label{defequi1:3}
  $3$ & $((P\ \Leftrightarrow \  Q)\ \Rightarrow \  (P\ \Leftrightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \Leftrightarrow \  Q)$ in \hyperref[defequi1:2]{$2$}
} \\
\label{defequi1:4}
  $4$ & $((P\ \Leftrightarrow \  Q)\ \Rightarrow \  ((P\ \Rightarrow \  Q)\ \wedge \  (Q\ \Rightarrow \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{equi}{equi} in \hyperref[defequi1:3]{$3$} at occurence $2$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Definition of an Equivalence 2. part:




\begin{thm}
\hypertarget{defequi2}{}
\begin{displaymath}
(((P\ \Rightarrow \  Q)\ \wedge \  (Q\ \Rightarrow \  P))\ \Rightarrow \  (P\ \Leftrightarrow \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{defequi2:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{defequi2:2}
  $2$ & $(A\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $A$ in \hyperref[defequi2:1]{$1$}
} \\
\label{defequi2:3}
  $3$ & $((P\ \Leftrightarrow \  Q)\ \Rightarrow \  (P\ \Leftrightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \Leftrightarrow \  Q)$ in \hyperref[defequi2:2]{$2$}
} \\
\label{defequi2:4}
  $4$ & $(((P\ \Rightarrow \  Q)\ \wedge \  (Q\ \Rightarrow \  P))\ \Rightarrow \  (P\ \Leftrightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule5}{use abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{equi}{equi} in \hyperref[defequi2:3]{$3$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



A simular formulation for the second axiom:




\begin{thm}
\hypertarget{hilb8}{}
\begin{displaymath}
(P\ \Rightarrow \  (Q\ \vee \  P))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb8:1}
  $1$ & $(P\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb8:2}
  $2$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{hilb8:3}
  $3$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb1}{hilb1} } \\
\label{hilb8:4}
  $4$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb8:3]{$3$}
} \\
\label{hilb8:5}
  $5$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb8:4]{$4$}
} \\
\label{hilb8:6}
  $6$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb8:5]{$5$}
} \\
\label{hilb8:7}
  $7$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \Rightarrow \  D)\ \Rightarrow \  (P\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb8:6]{$6$}
} \\
\label{hilb8:8}
  $8$ & $((D\ \Rightarrow \  (Q\ \vee \  P))\ \Rightarrow \  ((P\ \Rightarrow \  D)\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  P)$ in \hyperref[hilb8:7]{$7$}
} \\
\label{hilb8:9}
  $9$ & $(((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))\ \Rightarrow \  ((P\ \Rightarrow \  (P\ \vee \  Q))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  Q)$ in \hyperref[hilb8:8]{$8$}
} \\
\label{hilb8:10}
  $10$ & $((P\ \Rightarrow \  (P\ \vee \  Q))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb8:2]{$2$}, \hyperref[hilb8:9]{$9$}} \\
\label{hilb8:11}
  $11$ & $(P\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb8:1]{$1$}, \hyperref[hilb8:10]{$10$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



A technical lemma (equal to the third axiom):




\begin{thm}
\hypertarget{hilb9}{}
\begin{displaymath}
((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb9:1}
  $1$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



And another technical lemma (simular to the third axiom):




\begin{thm}
\hypertarget{hilb10}{}
\begin{displaymath}
((Q\ \vee \  P)\ \Rightarrow \  (P\ \vee \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb10:1}
  $1$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{hilb10:2}
  $2$ & $((P\ \vee \  A)\ \Rightarrow \  (A\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb10:1]{$1$}
} \\
\label{hilb10:3}
  $3$ & $((B\ \vee \  A)\ \Rightarrow \  (A\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb10:2]{$2$}
} \\
\label{hilb10:4}
  $4$ & $((B\ \vee \  P)\ \Rightarrow \  (P\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P$ in \hyperref[hilb10:3]{$3$}
} \\
\label{hilb10:5}
  $5$ & $((Q\ \vee \  P)\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb10:4]{$4$}
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



A technical lemma (equal to the first axiom):




\begin{thm}
\hypertarget{hilb11}{}
\begin{displaymath}
((P\ \vee \  P)\ \Rightarrow \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb11:1}
  $1$ & $((P\ \vee \  P)\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom1}{axiom1} } \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



A simple propositon that follows directly from the second axiom:




\begin{thm}
\hypertarget{hilb12}{}
\begin{displaymath}
(P\ \Rightarrow \  (P\ \vee \  P))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb12:1}
  $1$ & $(P\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb12:2}
  $2$ & $(P\ \Rightarrow \  (P\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[hilb12:1]{$1$}
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



This is a pre form for the associative law:




\begin{thm}
\hypertarget{hilb13}{}
\begin{displaymath}
((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb13:1}
  $1$ & $(P\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb8}{hilb8} } \\
\label{hilb13:2}
  $2$ & $(P\ \Rightarrow \  (B\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb13:1]{$1$}
} \\
\label{hilb13:3}
  $3$ & $(C\ \Rightarrow \  (B\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb13:2]{$2$}
} \\
\label{hilb13:4}
  $4$ & $(C\ \Rightarrow \  (P\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb13:3]{$3$}
} \\
\label{hilb13:5}
  $5$ & $(A\ \Rightarrow \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $A$ in \hyperref[hilb13:4]{$4$}
} \\
\label{hilb13:6}
  $6$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{hilb13:7}
  $7$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb13:6]{$6$}
} \\
\label{hilb13:8}
  $8$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb13:7]{$7$}
} \\
\label{hilb13:9}
  $9$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  D)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb13:8]{$8$}
} \\
\label{hilb13:10}
  $10$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((Q\ \vee \  D)\ \Rightarrow \  (Q\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb13:9]{$9$}
} \\
\label{hilb13:11}
  $11$ & $((D\ \Rightarrow \  (P\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  D)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  A)$ in \hyperref[hilb13:10]{$10$}
} \\
\label{hilb13:12}
  $12$ & $((A\ \Rightarrow \  (P\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  A)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $A$ in \hyperref[hilb13:11]{$11$}
} \\
\label{hilb13:13}
  $13$ & $((Q\ \vee \  A)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:5]{$5$}, \hyperref[hilb13:12]{$12$}} \\
\label{hilb13:14}
  $14$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb13:9]{$9$}
} \\
\label{hilb13:15}
  $15$ & $((D\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:14]{$14$}
} \\
\label{hilb13:16}
  $16$ & $(((Q\ \vee \  A)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(Q\ \vee \  A)$ in \hyperref[hilb13:15]{$15$}
} \\
\label{hilb13:17}
  $17$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:13]{$13$}, \hyperref[hilb13:16]{$16$}} \\
\label{hilb13:18}
  $18$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb9}{hilb9} } \\
\label{hilb13:19}
  $19$ & $((P\ \vee \  B)\ \Rightarrow \  (B\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb13:18]{$18$}
} \\
\label{hilb13:20}
  $20$ & $((C\ \vee \  B)\ \Rightarrow \  (B\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb13:19]{$19$}
} \\
\label{hilb13:21}
  $21$ & $((C\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:20]{$20$}
} \\
\label{hilb13:22}
  $22$ & $((P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $P$ in \hyperref[hilb13:21]{$21$}
} \\
\label{hilb13:23}
  $23$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{defimpl1}{defimpl1} } \\
\label{hilb13:24}
  $24$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (P\ \Rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{defimpl2}{defimpl2} } \\
\label{hilb13:25}
  $25$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  D)\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg (P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb13:9]{$9$}
} \\
\label{hilb13:26}
  $26$ & $((D\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))\ \Rightarrow \  ((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  D)\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)$ in \hyperref[hilb13:25]{$25$}
} \\
\label{hilb13:27}
  $27$ & $(((P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))\ \Rightarrow \  ((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$ in \hyperref[hilb13:26]{$26$}
} \\
\label{hilb13:28}
  $28$ & $((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:22]{$22$}, \hyperref[hilb13:27]{$27$}} \\
\label{hilb13:29}
  $29$ & $((P\ \Rightarrow \  B)\ \Rightarrow \  (\neg P\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb13:23]{$23$}
} \\
\label{hilb13:30}
  $30$ & $((C\ \Rightarrow \  B)\ \Rightarrow \  (\neg C\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb13:29]{$29$}
} \\
\label{hilb13:31}
  $31$ & $((C\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg C\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$ in \hyperref[hilb13:30]{$30$}
} \\
\label{hilb13:32}
  $32$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb13:31]{$31$}
} \\
\label{hilb13:33}
  $33$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb1}{hilb1} } \\
\label{hilb13:34}
  $34$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb13:33]{$33$}
} \\
\label{hilb13:35}
  $35$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb13:34]{$34$}
} \\
\label{hilb13:36}
  $36$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb13:35]{$35$}
} \\
\label{hilb13:37}
  $37$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$ in \hyperref[hilb13:36]{$36$}
} \\
\label{hilb13:38}
  $38$ & $((D\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))$ in \hyperref[hilb13:37]{$37$}
} \\
\label{hilb13:39}
  $39$ & $(((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$ in \hyperref[hilb13:38]{$38$}
} \\
\label{hilb13:40}
  $40$ & $((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:28]{$28$}, \hyperref[hilb13:39]{$39$}} \\
\label{hilb13:41}
  $41$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:32]{$32$}, \hyperref[hilb13:40]{$40$}} \\
\label{hilb13:42}
  $42$ & $((\neg P\ \vee \  B)\ \Rightarrow \  (P\ \Rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb13:24]{$24$}
} \\
\label{hilb13:43}
  $43$ & $((\neg C\ \vee \  B)\ \Rightarrow \  (C\ \Rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb13:42]{$42$}
} \\
\label{hilb13:44}
  $44$ & $((\neg C\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))\ \Rightarrow \  (C\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)$ in \hyperref[hilb13:43]{$43$}
} \\
\label{hilb13:45}
  $45$ & $((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb13:44]{$44$}
} \\
\label{hilb13:46}
  $46$ & $((D\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))$ in \hyperref[hilb13:37]{$37$}
} \\
\label{hilb13:47}
  $47$ & $(((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))$ in \hyperref[hilb13:46]{$46$}
} \\
\label{hilb13:48}
  $48$ & $((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:45]{$45$}, \hyperref[hilb13:47]{$47$}} \\
\label{hilb13:49}
  $49$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:41]{$41$}, \hyperref[hilb13:48]{$48$}} \\
\label{hilb13:50}
  $50$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:17]{$17$}, \hyperref[hilb13:49]{$49$}} \\
\label{hilb13:51}
  $51$ & $((P\ \vee \  A)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $(P\ \vee \  A)$ in \hyperref[hilb13:1]{$1$}
} \\
\label{hilb13:52}
  $52$ & $(P\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb13:53}
  $53$ & $(P\ \Rightarrow \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb13:52]{$52$}
} \\
\label{hilb13:54}
  $54$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \Rightarrow \  D)\ \Rightarrow \  (P\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb13:36]{$36$}
} \\
\label{hilb13:55}
  $55$ & $((D\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((P\ \Rightarrow \  D)\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:54]{$54$}
} \\
\label{hilb13:56}
  $56$ & $(((P\ \vee \  A)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((P\ \Rightarrow \  (P\ \vee \  A))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  A)$ in \hyperref[hilb13:55]{$55$}
} \\
\label{hilb13:57}
  $57$ & $((P\ \Rightarrow \  (P\ \vee \  A))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:51]{$51$}, \hyperref[hilb13:56]{$56$}} \\
\label{hilb13:58}
  $58$ & $(P\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:53]{$53$}, \hyperref[hilb13:57]{$57$}} \\
\label{hilb13:59}
  $59$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  D)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:9]{$9$}
} \\
\label{hilb13:60}
  $60$ & $((D\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  D)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:59]{$59$}
} \\
\label{hilb13:61}
  $61$ & $((P\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $P$ in \hyperref[hilb13:60]{$60$}
} \\
\label{hilb13:62}
  $62$ & $(((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:58]{$58$}, \hyperref[hilb13:61]{$61$}} \\
\label{hilb13:63}
  $63$ & $((P\ \vee \  P)\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb11}{hilb11} } \\
\label{hilb13:64}
  $64$ & $((B\ \vee \  B)\ \Rightarrow \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb13:63]{$63$}
} \\
\label{hilb13:65}
  $65$ & $(((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:64]{$64$}
} \\
\label{hilb13:66}
  $66$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  D)\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)$ in \hyperref[hilb13:9]{$9$}
} \\
\label{hilb13:67}
  $67$ & $((D\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  D)\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:66]{$66$}
} \\
\label{hilb13:68}
  $68$ & $((((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  ((\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$ in \hyperref[hilb13:67]{$67$}
} \\
\label{hilb13:69}
  $69$ & $((\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:65]{$65$}, \hyperref[hilb13:68]{$68$}} \\
\label{hilb13:70}
  $70$ & $((C\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg C\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$ in \hyperref[hilb13:30]{$30$}
} \\
\label{hilb13:71}
  $71$ & $((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)$ in \hyperref[hilb13:70]{$70$}
} \\
\label{hilb13:72}
  $72$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  D)\ \Rightarrow \  ((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$ in \hyperref[hilb13:36]{$36$}
} \\
\label{hilb13:73}
  $73$ & $((D\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  D)\ \Rightarrow \  ((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$ in \hyperref[hilb13:72]{$72$}
} \\
\label{hilb13:74}
  $74$ & $(((\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))\ \Rightarrow \  ((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$ in \hyperref[hilb13:73]{$73$}
} \\
\label{hilb13:75}
  $75$ & $(((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))\ \Rightarrow \  ((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:69]{$69$}, \hyperref[hilb13:74]{$74$}} \\
\label{hilb13:76}
  $76$ & $((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:71]{$71$}, \hyperref[hilb13:75]{$75$}} \\
\label{hilb13:77}
  $77$ & $((\neg C\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (C\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:43]{$43$}
} \\
\label{hilb13:78}
  $78$ & $((\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)$ in \hyperref[hilb13:77]{$77$}
} \\
\label{hilb13:79}
  $79$ & $((D\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  D)\ \Rightarrow \  ((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$ in \hyperref[hilb13:72]{$72$}
} \\
\label{hilb13:80}
  $80$ & $(((\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  ((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A)))$ in \hyperref[hilb13:79]{$79$}
} \\
\label{hilb13:81}
  $81$ & $(((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (\neg ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  ((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:78]{$78$}, \hyperref[hilb13:80]{$80$}} \\
\label{hilb13:82}
  $82$ & $((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))\ \Rightarrow \  (((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:76]{$76$}, \hyperref[hilb13:81]{$81$}} \\
\label{hilb13:83}
  $83$ & $(((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:62]{$62$}, \hyperref[hilb13:82]{$82$}} \\
\label{hilb13:84}
  $84$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb13:36]{$36$}
} \\
\label{hilb13:85}
  $85$ & $((D\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  (P\ \vee \  A))$ in \hyperref[hilb13:84]{$84$}
} \\
\label{hilb13:86}
  $86$ & $((((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)$ in \hyperref[hilb13:85]{$85$}
} \\
\label{hilb13:87}
  $87$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:83]{$83$}, \hyperref[hilb13:86]{$86$}} \\
\label{hilb13:88}
  $88$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb13:50]{$50$}, \hyperref[hilb13:87]{$87$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



The associative law for the disjunction (first direction):




\begin{thm}
\hypertarget{hilb14}{}
\begin{displaymath}
((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb14:1}
  $1$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb9}{hilb9} } \\
\label{hilb14:2}
  $2$ & $((P\ \vee \  B)\ \Rightarrow \  (B\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb14:1]{$1$}
} \\
\label{hilb14:3}
  $3$ & $((C\ \vee \  B)\ \Rightarrow \  (B\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb14:2]{$2$}
} \\
\label{hilb14:4}
  $4$ & $((C\ \vee \  A)\ \Rightarrow \  (A\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $A$ in \hyperref[hilb14:3]{$3$}
} \\
\label{hilb14:5}
  $5$ & $((Q\ \vee \  A)\ \Rightarrow \  (A\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $Q$ in \hyperref[hilb14:4]{$4$}
} \\
\label{hilb14:6}
  $6$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{hilb14:7}
  $7$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb14:6]{$6$}
} \\
\label{hilb14:8}
  $8$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb14:7]{$7$}
} \\
\label{hilb14:9}
  $9$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  D)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb14:8]{$8$}
} \\
\label{hilb14:10}
  $10$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb14:9]{$9$}
} \\
\label{hilb14:11}
  $11$ & $((D\ \Rightarrow \  (A\ \vee \  Q))\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(A\ \vee \  Q)$ in \hyperref[hilb14:10]{$10$}
} \\
\label{hilb14:12}
  $12$ & $(((Q\ \vee \  A)\ \Rightarrow \  (A\ \vee \  Q))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(Q\ \vee \  A)$ in \hyperref[hilb14:11]{$11$}
} \\
\label{hilb14:13}
  $13$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:5]{$5$}, \hyperref[hilb14:12]{$12$}} \\
\label{hilb14:14}
  $14$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{defimpl1}{defimpl1} } \\
\label{hilb14:15}
  $15$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (P\ \Rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{defimpl2}{defimpl2} } \\
\label{hilb14:16}
  $16$ & $((P\ \Rightarrow \  B)\ \Rightarrow \  (\neg P\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb14:14]{$14$}
} \\
\label{hilb14:17}
  $17$ & $((C\ \Rightarrow \  B)\ \Rightarrow \  (\neg C\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb14:16]{$16$}
} \\
\label{hilb14:18}
  $18$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb1}{hilb1} } \\
\label{hilb14:19}
  $19$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb14:18]{$18$}
} \\
\label{hilb14:20}
  $20$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb14:19]{$19$}
} \\
\label{hilb14:21}
  $21$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb14:20]{$20$}
} \\
\label{hilb14:22}
  $22$ & $((\neg P\ \vee \  B)\ \Rightarrow \  (P\ \Rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb14:15]{$15$}
} \\
\label{hilb14:23}
  $23$ & $((\neg C\ \vee \  B)\ \Rightarrow \  (C\ \Rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb14:22]{$22$}
} \\
\label{hilb14:24}
  $24$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb13}{hilb13} } \\
\label{hilb14:25}
  $25$ & $((P\ \vee \  (Q\ \vee \  B))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb14:24]{$24$}
} \\
\label{hilb14:26}
  $26$ & $((P\ \vee \  (C\ \vee \  B))\ \Rightarrow \  (C\ \vee \  (P\ \vee \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb14:25]{$25$}
} \\
\label{hilb14:27}
  $27$ & $((D\ \vee \  (C\ \vee \  B))\ \Rightarrow \  (C\ \vee \  (D\ \vee \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb14:26]{$26$}
} \\
\label{hilb14:28}
  $28$ & $((D\ \vee \  (C\ \vee \  Q))\ \Rightarrow \  (C\ \vee \  (D\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb14:27]{$27$}
} \\
\label{hilb14:29}
  $29$ & $((D\ \vee \  (A\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (D\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $A$ in \hyperref[hilb14:28]{$28$}
} \\
\label{hilb14:30}
  $30$ & $((P\ \vee \  (A\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $P$ in \hyperref[hilb14:29]{$29$}
} \\
\label{hilb14:31}
  $31$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb14:21]{$21$}
} \\
\label{hilb14:32}
  $32$ & $((D\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(A\ \vee \  (P\ \vee \  Q))$ in \hyperref[hilb14:31]{$31$}
} \\
\label{hilb14:33}
  $33$ & $(((P\ \vee \  (A\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  (A\ \vee \  Q))$ in \hyperref[hilb14:32]{$32$}
} \\
\label{hilb14:34}
  $34$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:30]{$30$}, \hyperref[hilb14:33]{$33$}} \\
\label{hilb14:35}
  $35$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:13]{$13$}, \hyperref[hilb14:34]{$34$}} \\
\label{hilb14:36}
  $36$ & $((C\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  Q)$ in \hyperref[hilb14:3]{$3$}
} \\
\label{hilb14:37}
  $37$ & $((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $A$ in \hyperref[hilb14:36]{$36$}
} \\
\label{hilb14:38}
  $38$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  D)\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg (P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb14:9]{$9$}
} \\
\label{hilb14:39}
  $39$ & $((D\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  ((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  D)\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb14:38]{$38$}
} \\
\label{hilb14:40}
  $40$ & $(((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  ((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(A\ \vee \  (P\ \vee \  Q))$ in \hyperref[hilb14:39]{$39$}
} \\
\label{hilb14:41}
  $41$ & $((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:37]{$37$}, \hyperref[hilb14:40]{$40$}} \\
\label{hilb14:42}
  $42$ & $((C\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg C\ \vee \  (A\ \vee \  (P\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(A\ \vee \  (P\ \vee \  Q))$ in \hyperref[hilb14:17]{$17$}
} \\
\label{hilb14:43}
  $43$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (A\ \vee \  (P\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb14:42]{$42$}
} \\
\label{hilb14:44}
  $44$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))$ in \hyperref[hilb14:21]{$21$}
} \\
\label{hilb14:45}
  $45$ & $((D\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A))$ in \hyperref[hilb14:44]{$44$}
} \\
\label{hilb14:46}
  $46$ & $(((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (A\ \vee \  (P\ \vee \  Q))))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (A\ \vee \  (P\ \vee \  Q)))$ in \hyperref[hilb14:45]{$45$}
} \\
\label{hilb14:47}
  $47$ & $((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  (A\ \vee \  (P\ \vee \  Q))))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:41]{$41$}, \hyperref[hilb14:46]{$46$}} \\
\label{hilb14:48}
  $48$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:43]{$43$}, \hyperref[hilb14:47]{$47$}} \\
\label{hilb14:49}
  $49$ & $((\neg C\ \vee \  ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  (C\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb14:23]{$23$}
} \\
\label{hilb14:50}
  $50$ & $((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb14:49]{$49$}
} \\
\label{hilb14:51}
  $51$ & $((D\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))$ in \hyperref[hilb14:44]{$44$}
} \\
\label{hilb14:52}
  $52$ & $(((\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  ((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A))$ in \hyperref[hilb14:51]{$51$}
} \\
\label{hilb14:53}
  $53$ & $((((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \vee \  ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  (((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:50]{$50$}, \hyperref[hilb14:52]{$52$}} \\
\label{hilb14:54}
  $54$ & $(((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  ((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:48]{$48$}, \hyperref[hilb14:53]{$53$}} \\
\label{hilb14:55}
  $55$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb14:35]{$35$}, \hyperref[hilb14:54]{$54$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



The associative law for the disjunction (second direction):




\begin{thm}
\hypertarget{hilb15}{}
\begin{displaymath}
(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb15:1}
  $1$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb14}{hilb14} } \\
\label{hilb15:2}
  $2$ & $((P\ \vee \  (Q\ \vee \  B))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb15:1]{$1$}
} \\
\label{hilb15:3}
  $3$ & $((P\ \vee \  (C\ \vee \  B))\ \Rightarrow \  ((P\ \vee \  C)\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb15:2]{$2$}
} \\
\label{hilb15:4}
  $4$ & $((D\ \vee \  (C\ \vee \  B))\ \Rightarrow \  ((D\ \vee \  C)\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb15:3]{$3$}
} \\
\label{hilb15:5}
  $5$ & $((D\ \vee \  (C\ \vee \  P))\ \Rightarrow \  ((D\ \vee \  C)\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb15:4]{$4$}
} \\
\label{hilb15:6}
  $6$ & $((D\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((D\ \vee \  Q)\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $Q$ in \hyperref[hilb15:5]{$5$}
} \\
\label{hilb15:7}
  $7$ & $((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $A$ in \hyperref[hilb15:6]{$6$}
} \\
\label{hilb15:8}
  $8$ & $((Q\ \vee \  P)\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb10}{hilb10} } \\
\label{hilb15:9}
  $9$ & $((B\ \vee \  P)\ \Rightarrow \  (P\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb15:8]{$8$}
} \\
\label{hilb15:10}
  $10$ & $((B\ \vee \  C)\ \Rightarrow \  (C\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb15:9]{$9$}
} \\
\label{hilb15:11}
  $11$ & $(((Q\ \vee \  P)\ \vee \  C)\ \Rightarrow \  (C\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(Q\ \vee \  P)$ in \hyperref[hilb15:10]{$10$}
} \\
\label{hilb15:12}
  $12$ & $(((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $A$ in \hyperref[hilb15:11]{$11$}
} \\
\label{hilb15:13}
  $13$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{defimpl1}{defimpl1} } \\
\label{hilb15:14}
  $14$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (P\ \Rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{defimpl2}{defimpl2} } \\
\label{hilb15:15}
  $15$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg Q\ \Rightarrow \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb7}{hilb7} } \\
\label{hilb15:16}
  $16$ & $((P\ \Rightarrow \  B)\ \Rightarrow \  (\neg B\ \Rightarrow \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb15:15]{$15$}
} \\
\label{hilb15:17}
  $17$ & $((C\ \Rightarrow \  B)\ \Rightarrow \  (\neg B\ \Rightarrow \  \neg C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb15:16]{$16$}
} \\
\label{hilb15:18}
  $18$ & $((C\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (\neg (A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  \neg C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(A\ \vee \  (Q\ \vee \  P))$ in \hyperref[hilb15:17]{$17$}
} \\
\label{hilb15:19}
  $19$ & $((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (\neg (A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  \neg ((Q\ \vee \  P)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:18]{$18$}
} \\
\label{hilb15:20}
  $20$ & $(\neg (A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  \neg ((Q\ \vee \  P)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:12]{$12$}, \hyperref[hilb15:19]{$19$}} \\
\label{hilb15:21}
  $21$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \vee \  P)\ \Rightarrow \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} } \\
\label{hilb15:22}
  $22$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb15:21]{$21$}
} \\
\label{hilb15:23}
  $23$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb15:22]{$22$}
} \\
\label{hilb15:24}
  $24$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  D)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb15:23]{$23$}
} \\
\label{hilb15:25}
  $25$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  D)\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((A\ \vee \  Q)\ \vee \  P)$ in \hyperref[hilb15:24]{$24$}
} \\
\label{hilb15:26}
  $26$ & $((D\ \Rightarrow \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  D)\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg ((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:25]{$25$}
} \\
\label{hilb15:27}
  $27$ & $((\neg (A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $\neg (A\ \vee \  (Q\ \vee \  P))$ in \hyperref[hilb15:26]{$26$}
} \\
\label{hilb15:28}
  $28$ & $((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:20]{$20$}, \hyperref[hilb15:27]{$27$}} \\
\label{hilb15:29}
  $29$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{hilb15:30}
  $30$ & $((P\ \vee \  B)\ \Rightarrow \  (B\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb15:29]{$29$}
} \\
\label{hilb15:31}
  $31$ & $((C\ \vee \  B)\ \Rightarrow \  (B\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb15:30]{$30$}
} \\
\label{hilb15:32}
  $32$ & $((C\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg ((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:31]{$31$}
} \\
\label{hilb15:33}
  $33$ & $((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((A\ \vee \  Q)\ \vee \  P)$ in \hyperref[hilb15:32]{$32$}
} \\
\label{hilb15:34}
  $34$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb1}{hilb1} } \\
\label{hilb15:35}
  $35$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb15:34]{$34$}
} \\
\label{hilb15:36}
  $36$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb15:35]{$35$}
} \\
\label{hilb15:37}
  $37$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb15:36]{$36$}
} \\
\label{hilb15:38}
  $38$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  D)\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:39}
  $39$ & $((D\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  D)\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:38]{$38$}
} \\
\label{hilb15:40}
  $40$ & $(((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A)))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))$ in \hyperref[hilb15:39]{$39$}
} \\
\label{hilb15:41}
  $41$ & $(((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A)))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:33]{$33$}, \hyperref[hilb15:40]{$40$}} \\
\label{hilb15:42}
  $42$ & $((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:28]{$28$}, \hyperref[hilb15:41]{$41$}} \\
\label{hilb15:43}
  $43$ & $((C\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((A\ \vee \  Q)\ \vee \  P)$ in \hyperref[hilb15:31]{$31$}
} \\
\label{hilb15:44}
  $44$ & $((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg (A\ \vee \  (Q\ \vee \  P))$ in \hyperref[hilb15:43]{$43$}
} \\
\label{hilb15:45}
  $45$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:46}
  $46$ & $((D\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:45]{$45$}
} \\
\label{hilb15:47}
  $47$ & $(((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P))))\ \Rightarrow \  ((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P)))$ in \hyperref[hilb15:46]{$46$}
} \\
\label{hilb15:48}
  $48$ & $(((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg (A\ \vee \  (Q\ \vee \  P))))\ \Rightarrow \  ((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:42]{$42$}, \hyperref[hilb15:47]{$47$}} \\
\label{hilb15:49}
  $49$ & $((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:44]{$44$}, \hyperref[hilb15:48]{$48$}} \\
\label{hilb15:50}
  $50$ & $((P\ \Rightarrow \  B)\ \Rightarrow \  (\neg P\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb15:13]{$13$}
} \\
\label{hilb15:51}
  $51$ & $((C\ \Rightarrow \  B)\ \Rightarrow \  (\neg C\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb15:50]{$50$}
} \\
\label{hilb15:52}
  $52$ & $((C\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg C\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((A\ \vee \  Q)\ \vee \  P)$ in \hyperref[hilb15:51]{$51$}
} \\
\label{hilb15:53}
  $53$ & $(((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(A\ \vee \  (Q\ \vee \  P))$ in \hyperref[hilb15:52]{$52$}
} \\
\label{hilb15:54}
  $54$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:55}
  $55$ & $((D\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:54]{$54$}
} \\
\label{hilb15:56}
  $56$ & $(((\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:55]{$55$}
} \\
\label{hilb15:57}
  $57$ & $((((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg (A\ \vee \  (Q\ \vee \  P))\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:49]{$49$}, \hyperref[hilb15:56]{$56$}} \\
\label{hilb15:58}
  $58$ & $(((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:53]{$53$}, \hyperref[hilb15:57]{$57$}} \\
\label{hilb15:59}
  $59$ & $((\neg P\ \vee \  B)\ \Rightarrow \  (P\ \Rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $B$ in \hyperref[hilb15:14]{$14$}
} \\
\label{hilb15:60}
  $60$ & $((\neg C\ \vee \  B)\ \Rightarrow \  (C\ \Rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $C$ in \hyperref[hilb15:59]{$59$}
} \\
\label{hilb15:61}
  $61$ & $((\neg C\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (C\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((A\ \vee \  Q)\ \vee \  P)$ in \hyperref[hilb15:60]{$60$}
} \\
\label{hilb15:62}
  $62$ & $((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:61]{$61$}
} \\
\label{hilb15:63}
  $63$ & $((D\ \Rightarrow \  (((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:54]{$54$}
} \\
\label{hilb15:64}
  $64$ & $(((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:63]{$63$}
} \\
\label{hilb15:65}
  $65$ & $((((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:62]{$62$}, \hyperref[hilb15:64]{$64$}} \\
\label{hilb15:66}
  $66$ & $(((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:58]{$58$}, \hyperref[hilb15:65]{$65$}} \\
\label{hilb15:67}
  $67$ & $(((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:7]{$7$}, \hyperref[hilb15:66]{$66$}} \\
\label{hilb15:68}
  $68$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((A\ \vee \  D)\ \Rightarrow \  (A\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $A$ in \hyperref[hilb15:24]{$24$}
} \\
\label{hilb15:69}
  $69$ & $((D\ \Rightarrow \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  D)\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  P)$ in \hyperref[hilb15:68]{$68$}
} \\
\label{hilb15:70}
  $70$ & $(((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  Q)$ in \hyperref[hilb15:69]{$69$}
} \\
\label{hilb15:71}
  $71$ & $((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:29]{$29$}, \hyperref[hilb15:70]{$70$}} \\
\label{hilb15:72}
  $72$ & $((C\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(Q\ \vee \  P)$ in \hyperref[hilb15:31]{$31$}
} \\
\label{hilb15:73}
  $73$ & $((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $A$ in \hyperref[hilb15:72]{$72$}
} \\
\label{hilb15:74}
  $74$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  D)\ \Rightarrow \  ((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(A\ \vee \  (P\ \vee \  Q))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:75}
  $75$ & $((D\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  D)\ \Rightarrow \  ((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:74]{$74$}
} \\
\label{hilb15:76}
  $76$ & $(((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  ((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(A\ \vee \  (Q\ \vee \  P))$ in \hyperref[hilb15:75]{$75$}
} \\
\label{hilb15:77}
  $77$ & $(((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (Q\ \vee \  P)))\ \Rightarrow \  ((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:73]{$73$}, \hyperref[hilb15:76]{$76$}} \\
\label{hilb15:78}
  $78$ & $((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:71]{$71$}, \hyperref[hilb15:77]{$77$}} \\
\label{hilb15:79}
  $79$ & $((C\ \vee \  A)\ \Rightarrow \  (A\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $A$ in \hyperref[hilb15:31]{$31$}
} \\
\label{hilb15:80}
  $80$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  Q)$ in \hyperref[hilb15:79]{$79$}
} \\
\label{hilb15:81}
  $81$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:82}
  $82$ & $((D\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  D)\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:81]{$81$}
} \\
\label{hilb15:83}
  $83$ & $(((A\ \vee \  (P\ \vee \  Q))\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(A\ \vee \  (P\ \vee \  Q))$ in \hyperref[hilb15:82]{$82$}
} \\
\label{hilb15:84}
  $84$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:78]{$78$}, \hyperref[hilb15:83]{$83$}} \\
\label{hilb15:85}
  $85$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:80]{$80$}, \hyperref[hilb15:84]{$84$}} \\
\label{hilb15:86}
  $86$ & $((C\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  \neg C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:17]{$17$}
} \\
\label{hilb15:87}
  $87$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  \neg ((P\ \vee \  Q)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:86]{$86$}
} \\
\label{hilb15:88}
  $88$ & $(\neg ((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  \neg ((P\ \vee \  Q)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:85]{$85$}, \hyperref[hilb15:87]{$87$}} \\
\label{hilb15:89}
  $89$ & $((D\ \Rightarrow \  \neg ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  D)\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg ((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:25]{$25$}
} \\
\label{hilb15:90}
  $90$ & $((\neg ((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  \neg ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $\neg ((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:89]{$89$}
} \\
\label{hilb15:91}
  $91$ & $((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:88]{$88$}, \hyperref[hilb15:90]{$90$}} \\
\label{hilb15:92}
  $92$ & $((C\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg ((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:31]{$31$}
} \\
\label{hilb15:93}
  $93$ & $((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((A\ \vee \  Q)\ \vee \  P)$ in \hyperref[hilb15:92]{$92$}
} \\
\label{hilb15:94}
  $94$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:95}
  $95$ & $((D\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:94]{$94$}
} \\
\label{hilb15:96}
  $96$ & $(((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A))$ in \hyperref[hilb15:95]{$95$}
} \\
\label{hilb15:97}
  $97$ & $(((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((P\ \vee \  Q)\ \vee \  A)))\ \Rightarrow \  ((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:93]{$93$}, \hyperref[hilb15:96]{$96$}} \\
\label{hilb15:98}
  $98$ & $((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:91]{$91$}, \hyperref[hilb15:97]{$97$}} \\
\label{hilb15:99}
  $99$ & $((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg ((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:43]{$43$}
} \\
\label{hilb15:100}
  $100$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:101}
  $101$ & $((D\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:100]{$100$}
} \\
\label{hilb15:102}
  $102$ & $(((((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A)))\ \Rightarrow \  ((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A))$ in \hyperref[hilb15:101]{$101$}
} \\
\label{hilb15:103}
  $103$ & $(((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((A\ \vee \  Q)\ \vee \  P)\ \vee \  \neg ((Q\ \vee \  P)\ \vee \  A)))\ \Rightarrow \  ((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:98]{$98$}, \hyperref[hilb15:102]{$102$}} \\
\label{hilb15:104}
  $104$ & $((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:99]{$99$}, \hyperref[hilb15:103]{$103$}} \\
\label{hilb15:105}
  $105$ & $((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((Q\ \vee \  P)\ \vee \  A)$ in \hyperref[hilb15:52]{$52$}
} \\
\label{hilb15:106}
  $106$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:107}
  $107$ & $((D\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:106]{$106$}
} \\
\label{hilb15:108}
  $108$ & $(((\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:107]{$107$}
} \\
\label{hilb15:109}
  $109$ & $(((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((Q\ \vee \  P)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:104]{$104$}, \hyperref[hilb15:108]{$108$}} \\
\label{hilb15:110}
  $110$ & $((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:105]{$105$}, \hyperref[hilb15:109]{$109$}} \\
\label{hilb15:111}
  $111$ & $((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:61]{$61$}
} \\
\label{hilb15:112}
  $112$ & $((D\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:106]{$106$}
} \\
\label{hilb15:113}
  $113$ & $(((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  (((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:112]{$112$}
} \\
\label{hilb15:114}
  $114$ & $(((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:111]{$111$}, \hyperref[hilb15:113]{$113$}} \\
\label{hilb15:115}
  $115$ & $((((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:110]{$110$}, \hyperref[hilb15:114]{$114$}} \\
\label{hilb15:116}
  $116$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:67]{$67$}, \hyperref[hilb15:115]{$115$}} \\
\label{hilb15:117}
  $117$ & $((C\ \vee \  P)\ \Rightarrow \  (P\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb15:31]{$31$}
} \\
\label{hilb15:118}
  $118$ & $(((A\ \vee \  Q)\ \vee \  P)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(A\ \vee \  Q)$ in \hyperref[hilb15:117]{$117$}
} \\
\label{hilb15:119}
  $119$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  D)\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg ((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:24]{$24$}
} \\
\label{hilb15:120}
  $120$ & $((D\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  ((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  D)\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  (A\ \vee \  Q))$ in \hyperref[hilb15:119]{$119$}
} \\
\label{hilb15:121}
  $121$ & $((((A\ \vee \  Q)\ \vee \  P)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  ((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $((A\ \vee \  Q)\ \vee \  P)$ in \hyperref[hilb15:120]{$120$}
} \\
\label{hilb15:122}
  $122$ & $((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:118]{$118$}, \hyperref[hilb15:121]{$121$}} \\
\label{hilb15:123}
  $123$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:52]{$52$}
} \\
\label{hilb15:124}
  $124$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:125}
  $125$ & $((D\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))$ in \hyperref[hilb15:124]{$124$}
} \\
\label{hilb15:126}
  $126$ & $(((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P))$ in \hyperref[hilb15:125]{$125$}
} \\
\label{hilb15:127}
  $127$ & $(((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  ((A\ \vee \  Q)\ \vee \  P)))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:122]{$122$}, \hyperref[hilb15:126]{$126$}} \\
\label{hilb15:128}
  $128$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:123]{$123$}, \hyperref[hilb15:127]{$127$}} \\
\label{hilb15:129}
  $129$ & $((\neg C\ \vee \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (C\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (A\ \vee \  Q))$ in \hyperref[hilb15:60]{$60$}
} \\
\label{hilb15:130}
  $130$ & $((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:129]{$129$}
} \\
\label{hilb15:131}
  $131$ & $((D\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  D)\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))$ in \hyperref[hilb15:124]{$124$}
} \\
\label{hilb15:132}
  $132$ & $(((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))$ in \hyperref[hilb15:131]{$131$}
} \\
\label{hilb15:133}
  $133$ & $(((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:130]{$130$}, \hyperref[hilb15:132]{$132$}} \\
\label{hilb15:134}
  $134$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:128]{$128$}, \hyperref[hilb15:133]{$133$}} \\
\label{hilb15:135}
  $135$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:116]{$116$}, \hyperref[hilb15:134]{$134$}} \\
\label{hilb15:136}
  $136$ & $((C\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  C))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb15:31]{$31$}
} \\
\label{hilb15:137}
  $137$ & $((A\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $A$ in \hyperref[hilb15:136]{$136$}
} \\
\label{hilb15:138}
  $138$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb15:24]{$24$}
} \\
\label{hilb15:139}
  $139$ & $((D\ \Rightarrow \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \vee \  A)$ in \hyperref[hilb15:138]{$138$}
} \\
\label{hilb15:140}
  $140$ & $(((A\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  (A\ \vee \  Q))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(A\ \vee \  Q)$ in \hyperref[hilb15:139]{$139$}
} \\
\label{hilb15:141}
  $141$ & $((P\ \vee \  (A\ \vee \  Q))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:137]{$137$}, \hyperref[hilb15:140]{$140$}} \\
\label{hilb15:142}
  $142$ & $((D\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))\ \Rightarrow \  ((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  D)\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb15:119]{$119$}
} \\
\label{hilb15:143}
  $143$ & $(((P\ \vee \  (A\ \vee \  Q))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))\ \Rightarrow \  ((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  (A\ \vee \  Q))$ in \hyperref[hilb15:142]{$142$}
} \\
\label{hilb15:144}
  $144$ & $((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:141]{$141$}, \hyperref[hilb15:143]{$143$}} \\
\label{hilb15:145}
  $145$ & $((C\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg C\ \vee \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (A\ \vee \  Q))$ in \hyperref[hilb15:51]{$51$}
} \\
\label{hilb15:146}
  $146$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:145]{$145$}
} \\
\label{hilb15:147}
  $147$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  D)\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))$ in \hyperref[hilb15:37]{$37$}
} \\
\label{hilb15:148}
  $148$ & $((D\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  D)\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A)))$ in \hyperref[hilb15:147]{$147$}
} \\
\label{hilb15:149}
  $149$ & $(((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q)))$ in \hyperref[hilb15:148]{$148$}
} \\
\label{hilb15:150}
  $150$ & $(((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (A\ \vee \  Q))))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:144]{$144$}, \hyperref[hilb15:149]{$149$}} \\
\label{hilb15:151}
  $151$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:146]{$146$}, \hyperref[hilb15:150]{$150$}} \\
\label{hilb15:152}
  $152$ & $((\neg C\ \vee \  (P\ \vee \  (Q\ \vee \  A)))\ \Rightarrow \  (C\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \vee \  A))$ in \hyperref[hilb15:60]{$60$}
} \\
\label{hilb15:153}
  $153$ & $((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \vee \  A)$ in \hyperref[hilb15:152]{$152$}
} \\
\label{hilb15:154}
  $154$ & $((D\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  D)\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))$ in \hyperref[hilb15:147]{$147$}
} \\
\label{hilb15:155}
  $155$ & $(((\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))\ \Rightarrow \  (((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A)))$ in \hyperref[hilb15:154]{$154$}
} \\
\label{hilb15:156}
  $156$ & $(((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \vee \  (P\ \vee \  (Q\ \vee \  A))))\ \Rightarrow \  ((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:153]{$153$}, \hyperref[hilb15:155]{$155$}} \\
\label{hilb15:157}
  $157$ & $((((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))\ \Rightarrow \  (((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:151]{$151$}, \hyperref[hilb15:156]{$156$}} \\
\label{hilb15:158}
  $158$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb15:135]{$135$}, \hyperref[hilb15:157]{$157$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Another consequence from hilb13 is the exchange of preconditions:




\begin{thm}
\hypertarget{hilb16}{}
\begin{displaymath}
((P\ \Rightarrow \  (Q\ \Rightarrow \  A))\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \Rightarrow \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb16:1}
  $1$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb13}{hilb13} } \\
\label{hilb16:2}
  $2$ & $((P\ \vee \  (Q\ \vee \  B))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb16:1]{$1$}
} \\
\label{hilb16:3}
  $3$ & $((P\ \vee \  (C\ \vee \  B))\ \Rightarrow \  (C\ \vee \  (P\ \vee \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb16:2]{$2$}
} \\
\label{hilb16:4}
  $4$ & $((D\ \vee \  (C\ \vee \  B))\ \Rightarrow \  (C\ \vee \  (D\ \vee \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb16:3]{$3$}
} \\
\label{hilb16:5}
  $5$ & $((D\ \vee \  (C\ \vee \  A))\ \Rightarrow \  (C\ \vee \  (D\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $A$ in \hyperref[hilb16:4]{$4$}
} \\
\label{hilb16:6}
  $6$ & $((D\ \vee \  (\neg Q\ \vee \  A))\ \Rightarrow \  (\neg Q\ \vee \  (D\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg Q$ in \hyperref[hilb16:5]{$5$}
} \\
\label{hilb16:7}
  $7$ & $((\neg P\ \vee \  (\neg Q\ \vee \  A))\ \Rightarrow \  (\neg Q\ \vee \  (\neg P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $\neg P$ in \hyperref[hilb16:6]{$6$}
} \\
\label{hilb16:8}
  $8$ & $((P\ \Rightarrow \  (\neg Q\ \vee \  A))\ \Rightarrow \  (\neg Q\ \vee \  (\neg P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb16:7]{$7$} at occurence $1$
} \\
\label{hilb16:9}
  $9$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  A))\ \Rightarrow \  (\neg Q\ \vee \  (\neg P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb16:8]{$8$} at occurence $1$
} \\
\label{hilb16:10}
  $10$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  A))\ \Rightarrow \  (Q\ \Rightarrow \  (\neg P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb16:9]{$9$} at occurence $1$
} \\
\label{hilb16:11}
  $11$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  A))\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \Rightarrow \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb16:10]{$10$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



An analogus form for \ref{hilb16}:




\begin{thm}
\hypertarget{hilb17}{}
\begin{displaymath}
((Q\ \Rightarrow \  (P\ \Rightarrow \  A))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \Rightarrow \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb17:1}
  $1$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  A))\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \Rightarrow \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb16}{hilb16} } \\
\label{hilb17:2}
  $2$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  B))\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb17:1]{$1$}
} \\
\label{hilb17:3}
  $3$ & $((P\ \Rightarrow \  (C\ \Rightarrow \  B))\ \Rightarrow \  (C\ \Rightarrow \  (P\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb17:2]{$2$}
} \\
\label{hilb17:4}
  $4$ & $((D\ \Rightarrow \  (C\ \Rightarrow \  B))\ \Rightarrow \  (C\ \Rightarrow \  (D\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb17:3]{$3$}
} \\
\label{hilb17:5}
  $5$ & $((D\ \Rightarrow \  (C\ \Rightarrow \  A))\ \Rightarrow \  (C\ \Rightarrow \  (D\ \Rightarrow \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $A$ in \hyperref[hilb17:4]{$4$}
} \\
\label{hilb17:6}
  $6$ & $((D\ \Rightarrow \  (P\ \Rightarrow \  A))\ \Rightarrow \  (P\ \Rightarrow \  (D\ \Rightarrow \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $P$ in \hyperref[hilb17:5]{$5$}
} \\
\label{hilb17:7}
  $7$ & $((Q\ \Rightarrow \  (P\ \Rightarrow \  A))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \Rightarrow \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $Q$ in \hyperref[hilb17:6]{$6$}
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}

\section*{}
This module used by the following modules:

\mbox{}
\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & prophilbert2 \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{prophilbert2_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{prophilbert2_1.00.00_1.00.00.pdf}  \\
\end{longtable}

\end{document}