% -*- TeX:EN -*-
%%% ====================================================================
%%% $RCSfile: Module2Latex.java,v $
%%% $Revision: 1.28 $
%%% ====================================================================
%%%
%%% Generated by class com.meyling.principia.latex.Module2Latex
%%% at 2004-09-26T23:33:09+0200.
%%%
%%% Project Hilbert II - http://www.qedeq.org
%%% Copyright 2001, 2002, 2003, 2004 Michael Meyling (mime@qedeq.org)
%%%
%%% This file is part of *Principia Mathematica II*, the prototype of
%%% Hilbert II.
%%%
%%% Permission is granted to copy, distribute and/or modify this document
%%% under the terms of the GNU Free Documentation License, Version 1.2
%%% or any later version published by the Free Software Foundation;
%%% with no Invariant Sections, no Front-Cover Texts, and no
%%% Back-Cover Texts.
%%%

\documentclass[a4paper]{article}

\usepackage{amsmath,amsthm,amsfonts}
\usepackage[]{color}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{varioref}
\usepackage[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


\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}

\setlength{\parindent}{0pt}
\frenchspacing \sloppy
\pagestyle{headings}

\title{First theorems of Propositional Calculus}
\author{Michael Meyling}
\date{\tt <module@qedeq.org>}


\begin{document}

\maketitle

\setlongtables



{\small
This document is part of the project ``Hilbert II''.
To get more information about this project look at:\\
\mbox{\url{http://www.qedeq.org}}.


Permission is granted to copy, distribute and/or modify this document
under the terms of the GNU Free Documentation License, Version 1.2
or any later version published by the Free Software Foundation;
with no Invariant Sections, no Front-Cover Texts, and no
Back-Cover Texts. See also under \url{http://www.gnu.org/copyleft/}
}


\section*{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)


\section*{Specification}

This document has the following specification:

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

\medskip

Author of this module: 
\begin{longtable}[h!]{l@{\extracolsep{\fill}}l}
Michael Meyling & mime@qedeq.org \\
\end{longtable}




\section*{References}

This document uses the results of the following documents:

\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}


\section*{Content}




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




\begin{thm}[hilb1]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}


This proposition is the form for the Hypothetical Syllogism.



\bigskip




The self implication could be derived:




\begin{thm}[hilb2]
\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$}} \\
 & & \qedhere
\end{longtable}
\end{proof}



One form of the classical `tertium non datur'




\begin{thm}[hilb3]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The standard form of the excluded middle:




\begin{thm}[hilb4]
\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$}} \\
 & & \qedhere
\end{longtable}
\end{proof}



Double negation is implicated:




\begin{thm}[hilb5]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The reverse is also true:




\begin{thm}[hilb6]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The correct reverse of an implication:




\begin{thm}[hilb7]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of an Implication 1. part:




\begin{thm}[defimpl1]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of an Implication 2. part:




\begin{thm}[defimpl2]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of a Conjunction 1. part:




\begin{thm}[defand1]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of a Conjunction 2. part:




\begin{thm}[defand2]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of an Equivalence 1. part:




\begin{thm}[defequi1]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Definition of an Equivalence 2. part:




\begin{thm}[defequi2]
\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$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



A simular formulation for the second axiom:




\begin{thm}[hilb8]
\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$}} \\
 & & \qedhere
\end{longtable}
\end{proof}



A technical lemma (equal to the third axiom):




\begin{thm}[hilb9]
\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} } \\
 & & \qedhere
\end{longtable}
\end{proof}



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




\begin{thm}[hilb10]
\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$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



A technical lemma (equal to the first axiom):




\begin{thm}[hilb11]
\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} } \\
 & & \qedhere
\end{longtable}
\end{proof}



A simple propositon that follows directly from the second axiom:




\begin{thm}[hilb12]
\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$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



This is a pre form for the associative law:




\begin{thm}[hilb13]
\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$}} \\
 & & \qedhere
\end{longtable}
\end{proof}



The associative law for the disjunction (first direction):




\begin{thm}[hilb14]
\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$}} \\
 & & \qedhere
\end{longtable}
\end{proof}



The associative law for the disjunction (second direction):




\begin{thm}[hilb15]
\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