% -*- TeX:EN -*-
%%% ====================================================================
%%% $RCSfile: Module2Latex.java,v $
%%% $Revision: 1.28 $
%%% ====================================================================
%%%
%%% Generated by class com.meyling.principia.latex.Module2Latex
%%% at 2004-09-26T23:33:10+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{prophilbert2_1.00.00_1.02.00.qedeq}
\hyperbaseurl{prophilbert2_1.00.00_1.02.00.qedeq}
\makeatother

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

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

\title{Further 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 proofs of popositional 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: & prophilbert2 \\
Version: & 1.00.00 \\
Rule version: & 1.02.00 \\
Orgin: & \url{http://www.qedeq.org/0_00_53/prophilbert2_1.00.00_1.02.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: & prophilbert1 \\
Version: & 1.00.00 \\
Rule version: & 1.02.00 \\
Orgin: & \url{prophilbert1_1.00.00_1.02.00.qedeq}  \\
pdf: & \url{prophilbert1_1.00.00_1.02.00.pdf}  \\
\end{longtable}


\section*{Content}




Negation of a conjunction:




\begin{thm}[hilb18]
\hypertarget{hilb18}{}
\begin{displaymath}
\neg (P\ \wedge \  Q)\ \rightarrow \  (\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{hilb18:1}
  $1$ & $\neg \neg P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb6}{hilb6} } \\
\label{hilb18:2}
  $2$ & $\neg \neg Q\ \rightarrow \  Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb18:1]{$1$}
} \\
\label{hilb18:3}
  $3$ & $\neg \neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  (\neg P\ \vee \  \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $\neg P\ \vee \  \neg Q$ in \hyperref[hilb18:2]{$2$}
} \\
\label{hilb18:4}
  $4$ & $\neg (P\ \wedge \  Q)\ \rightarrow \  (\neg P\ \vee \  \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb18:3]{$3$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The reverse of a negation of a conjunction:




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



Negation of a disjunction:




\begin{thm}[hilb20]
\hypertarget{hilb20}{}
\begin{displaymath}
\neg (P\ \vee \  Q)\ \rightarrow \  (\neg P\ \wedge \  \neg Q)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb20:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb2}{hilb2} } \\
\label{hilb20:2}
  $2$ & $Q\ \rightarrow \  Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb20:1]{$1$}
} \\
\label{hilb20:3}
  $3$ & $\neg (P\ \vee \  Q)\ \rightarrow \  \neg (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $\neg (P\ \vee \  Q)$ in \hyperref[hilb20:2]{$2$}
} \\
\label{hilb20:4}
  $4$ & $\neg (P\ \vee \  Q)\ \rightarrow \  \neg (\neg \neg P\ \vee \  Q)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb20:3]{$3$} at \hyperref[hilb20:8]{$8$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb20:5}
  $5$ & $\neg (P\ \vee \  Q)\ \rightarrow \  \neg (\neg \neg P\ \vee \  \neg \neg Q)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb20:4]{$4$} at \hyperref[hilb20:11]{$11$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb20:6}
  $6$ & $\neg (P\ \vee \  Q)\ \rightarrow \  (\neg P\ \wedge \  \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb20:5]{$5$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Reverse of a negation of a disjunction:




\begin{thm}[hilb21]
\hypertarget{hilb21}{}
\begin{displaymath}
(\neg P\ \wedge \  \neg 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{hilb21:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb2}{hilb2} } \\
\label{hilb21:2}
  $2$ & $Q\ \rightarrow \  Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb21:1]{$1$}
} \\
\label{hilb21:3}
  $3$ & $\neg (P\ \vee \  Q)\ \rightarrow \  \neg (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $\neg (P\ \vee \  Q)$ in \hyperref[hilb21:2]{$2$}
} \\
\label{hilb21:4}
  $4$ & $\neg (\neg \neg P\ \vee \  Q)\ \rightarrow \  \neg (P\ \vee \  Q)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb21:3]{$3$} at \hyperref[hilb21:4]{$4$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb21:5}
  $5$ & $\neg (\neg \neg P\ \vee \  \neg \neg Q)\ \rightarrow \  \neg (P\ \vee \  Q)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb21:4]{$4$} at \hyperref[hilb21:7]{$7$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb21:6}
  $6$ & $(\neg P\ \wedge \  \neg Q)\ \rightarrow \  \neg (P\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb21:5]{$5$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The Conjunction is commutative:




\begin{thm}[hilb22]
\hypertarget{hilb22}{}
\begin{displaymath}
(P\ \wedge \  Q)\ \rightarrow \  (Q\ \wedge \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb22:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb2}{hilb2} } \\
\label{hilb22:2}
  $2$ & $Q\ \rightarrow \  Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb22:1]{$1$}
} \\
\label{hilb22:3}
  $3$ & $(P\ \wedge \  Q)\ \rightarrow \  (P\ \wedge \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P\ \wedge \  Q$ in \hyperref[hilb22:2]{$2$}
} \\
\label{hilb22: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[hilb22:3]{$3$} at occurence $2$
} \\
\label{hilb22:5}
  $5$ & $(P\ \wedge \  Q)\ \rightarrow \  \neg (\neg Q\ \vee \  \neg P)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb22:4]{$4$} at \hyperref[hilb22:1]{$1$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb9}{hilb9}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb9}{hilb9} 
} \\
\label{hilb22:6}
  $6$ & $(P\ \wedge \  Q)\ \rightarrow \  (Q\ \wedge \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb22:5]{$5$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



A technical lemma that is simular to the previous one:




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



Reduction of a conjunction:




\begin{thm}[hilb24]
\hypertarget{hilb24}{}
\begin{displaymath}
(P\ \wedge \  Q)\ \rightarrow \  P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb24: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{hilb24:2}
  $2$ & $P\ \rightarrow \  (P\ \vee \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb24:1]{$1$}
} \\
\label{hilb24:3}
  $3$ & $B\ \rightarrow \  (B\ \vee \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb24:2]{$2$}
} \\
\label{hilb24:4}
  $4$ & $B\ \rightarrow \  (B\ \vee \  \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg Q$ in \hyperref[hilb24:3]{$3$}
} \\
\label{hilb24:5}
  $5$ & $\neg P\ \rightarrow \  (\neg P\ \vee \  \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg P$ in \hyperref[hilb24:4]{$4$}
} \\
\label{hilb24:6}
  $6$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (\neg Q\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb7}{hilb7} } \\
\label{hilb24:7}
  $7$ & $(P\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb24:6]{$6$}
} \\
\label{hilb24:8}
  $8$ & $(B\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb24:7]{$7$}
} \\
\label{hilb24:9}
  $9$ & $(B\ \rightarrow \  (\neg P\ \vee \  \neg Q))\ \rightarrow \  (\neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $\neg P\ \vee \  \neg Q$ in \hyperref[hilb24:8]{$8$}
} \\
\label{hilb24:10}
  $10$ & $(\neg P\ \rightarrow \  (\neg P\ \vee \  \neg Q))\ \rightarrow \  (\neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg P$ in \hyperref[hilb24:9]{$9$}
} \\
\label{hilb24:11}
  $11$ & $\neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  \neg \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb24:5]{$5$}, \hyperref[hilb24:10]{$10$}} \\
\label{hilb24:12}
  $12$ & $(P\ \wedge \  Q)\ \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}{}{and}{and} in \hyperref[hilb24:11]{$11$} at occurence $1$
} \\
\label{hilb24:13}
  $13$ & $(P\ \wedge \  Q)\ \rightarrow \  P$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb24:12]{$12$} at \hyperref[hilb24:1]{$1$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb6}{hilb6}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb6}{hilb6} 
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Another form of a reduction of a conjunction:




\begin{thm}[hilb25]
\hypertarget{hilb25}{}
\begin{displaymath}
(P\ \wedge \  Q)\ \rightarrow \  Q\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb25:1}
  $1$ & $(P\ \wedge \  Q)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb24}{hilb24} } \\
\label{hilb25:2}
  $2$ & $(P\ \wedge \  A)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb25:1]{$1$}
} \\
\label{hilb25:3}
  $3$ & $(B\ \wedge \  A)\ \rightarrow \  B$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb25:2]{$2$}
} \\
\label{hilb25:4}
  $4$ & $(B\ \wedge \  P)\ \rightarrow \  B$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P$ in \hyperref[hilb25:3]{$3$}
} \\
\label{hilb25:5}
  $5$ & $(Q\ \wedge \  P)\ \rightarrow \  Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb25:4]{$4$}
} \\
\label{hilb25:6}
  $6$ & $(P\ \wedge \  Q)\ \rightarrow \  Q$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb25:5]{$5$} at \hyperref[hilb25:1]{$1$} of \hyperref{}{}{hilb22}{hilb22}  with \hyperref{}{}{hilb22}{hilb22} 
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The conjunction is associative too (first implication):




\begin{thm}[hilb26]
\hypertarget{hilb26}{}
\begin{displaymath}
(P\ \wedge \  (Q\ \wedge \  A))\ \rightarrow \  ((P\ \wedge \  Q)\ \wedge \  A)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb26: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{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb15}{hilb15} } \\
\label{hilb26:2}
  $2$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (\neg Q\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb7}{hilb7} } \\
\label{hilb26:3}
  $3$ & $(P\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb26:2]{$2$}
} \\
\label{hilb26:4}
  $4$ & $(B\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb26:3]{$3$}
} \\
\label{hilb26:5}
  $5$ & $(B\ \rightarrow \  (P\ \vee \  (Q\ \vee \  A)))\ \rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P\ \vee \  (Q\ \vee \  A)$ in \hyperref[hilb26:4]{$4$}
} \\
\label{hilb26:6}
  $6$ & $(((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  (P\ \vee \  (Q\ \vee \  A)))\ \rightarrow \  (\neg (P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  \neg ((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[hilb26:5]{$5$}
} \\
\label{hilb26:7}
  $7$ & $\neg (P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  \neg ((P\ \vee \  Q)\ \vee \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb26:1]{$1$}, \hyperref[hilb26:6]{$6$}} \\
\label{hilb26:8}
  $8$ & $\neg (P\ \vee \  \neg \neg (Q\ \vee \  A))\ \rightarrow \  \neg ((P\ \vee \  Q)\ \vee \  A)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb26:7]{$7$} at \hyperref[hilb26:5]{$5$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb26:9}
  $9$ & $\neg (P\ \vee \  \neg \neg (Q\ \vee \  A))\ \rightarrow \  \neg (\neg \neg (P\ \vee \  Q)\ \vee \  A)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb26:8]{$8$} at \hyperref[hilb26:12]{$12$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb26:10}
  $10$ & $\neg (P\ \vee \  \neg \neg (Q\ \vee \  B))\ \rightarrow \  \neg (\neg \neg (P\ \vee \  Q)\ \vee \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb26:9]{$9$}
} \\
\label{hilb26:11}
  $11$ & $\neg (P\ \vee \  \neg \neg (C\ \vee \  B))\ \rightarrow \  \neg (\neg \neg (P\ \vee \  C)\ \vee \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb26:10]{$10$}
} \\
\label{hilb26:12}
  $12$ & $\neg (D\ \vee \  \neg \neg (C\ \vee \  B))\ \rightarrow \  \neg (\neg \neg (D\ \vee \  C)\ \vee \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb26:11]{$11$}
} \\
\label{hilb26:13}
  $13$ & $\neg (D\ \vee \  \neg \neg (C\ \vee \  \neg A))\ \rightarrow \  \neg (\neg \neg (D\ \vee \  C)\ \vee \  \neg A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg A$ in \hyperref[hilb26:12]{$12$}
} \\
\label{hilb26:14}
  $14$ & $\neg (D\ \vee \  \neg \neg (\neg Q\ \vee \  \neg A))\ \rightarrow \  \neg (\neg \neg (D\ \vee \  \neg Q)\ \vee \  \neg A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg Q$ in \hyperref[hilb26:13]{$13$}
} \\
\label{hilb26:15}
  $15$ & $\neg (\neg P\ \vee \  \neg \neg (\neg Q\ \vee \  \neg A))\ \rightarrow \  \neg (\neg \neg (\neg P\ \vee \  \neg Q)\ \vee \  \neg A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $\neg P$ in \hyperref[hilb26:14]{$14$}
} \\
\label{hilb26:16}
  $16$ & $(P\ \wedge \  \neg (\neg Q\ \vee \  \neg A))\ \rightarrow \  \neg (\neg \neg (\neg P\ \vee \  \neg Q)\ \vee \  \neg A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb26:15]{$15$} at occurence $1$
} \\
\label{hilb26:17}
  $17$ & $(P\ \wedge \  (Q\ \wedge \  A))\ \rightarrow \  \neg (\neg \neg (\neg P\ \vee \  \neg Q)\ \vee \  \neg A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb26:16]{$16$} at occurence $1$
} \\
\label{hilb26:18}
  $18$ & $(P\ \wedge \  (Q\ \wedge \  A))\ \rightarrow \  (\neg (\neg P\ \vee \  \neg Q)\ \wedge \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb26:17]{$17$} at occurence $1$
} \\
\label{hilb26:19}
  $19$ & $(P\ \wedge \  (Q\ \wedge \  A))\ \rightarrow \  ((P\ \wedge \  Q)\ \wedge \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb26:18]{$18$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



The conjunction is associative (second implication):




\begin{thm}[hilb27]
\hypertarget{hilb27}{}
\begin{displaymath}
((P\ \wedge \  Q)\ \wedge \  A)\ \rightarrow \  (P\ \wedge \  (Q\ \wedge \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb27: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{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb14}{hilb14} } \\
\label{hilb27:2}
  $2$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (\neg Q\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb7}{hilb7} } \\
\label{hilb27:3}
  $3$ & $(P\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb27:2]{$2$}
} \\
\label{hilb27:4}
  $4$ & $(B\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb27:3]{$3$}
} \\
\label{hilb27:5}
  $5$ & $(B\ \rightarrow \  ((P\ \vee \  Q)\ \vee \  A))\ \rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \vee \  Q)\ \vee \  A$ in \hyperref[hilb27:4]{$4$}
} \\
\label{hilb27:6}
  $6$ & $((P\ \vee \  (Q\ \vee \  A))\ \rightarrow \  ((P\ \vee \  Q)\ \vee \  A))\ \rightarrow \  (\neg ((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  \neg (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[hilb27:5]{$5$}
} \\
\label{hilb27:7}
  $7$ & $\neg ((P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  \neg (P\ \vee \  (Q\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb27:1]{$1$}, \hyperref[hilb27:6]{$6$}} \\
\label{hilb27:8}
  $8$ & $\neg (\neg \neg (P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  \neg (P\ \vee \  (Q\ \vee \  A))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb27:7]{$7$} at \hyperref[hilb27:4]{$4$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb27:9}
  $9$ & $\neg (\neg \neg (P\ \vee \  Q)\ \vee \  A)\ \rightarrow \  \neg (P\ \vee \  \neg \neg (Q\ \vee \  A))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb27:8]{$8$} at \hyperref[hilb27:13]{$13$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb27:10}
  $10$ & $\neg (\neg \neg (P\ \vee \  Q)\ \vee \  B)\ \rightarrow \  \neg (P\ \vee \  \neg \neg (Q\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb27:9]{$9$}
} \\
\label{hilb27:11}
  $11$ & $\neg (\neg \neg (P\ \vee \  C)\ \vee \  B)\ \rightarrow \  \neg (P\ \vee \  \neg \neg (C\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb27:10]{$10$}
} \\
\label{hilb27:12}
  $12$ & $\neg (\neg \neg (D\ \vee \  C)\ \vee \  B)\ \rightarrow \  \neg (D\ \vee \  \neg \neg (C\ \vee \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb27:11]{$11$}
} \\
\label{hilb27:13}
  $13$ & $\neg (\neg \neg (D\ \vee \  C)\ \vee \  \neg A)\ \rightarrow \  \neg (D\ \vee \  \neg \neg (C\ \vee \  \neg A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg A$ in \hyperref[hilb27:12]{$12$}
} \\
\label{hilb27:14}
  $14$ & $\neg (\neg \neg (D\ \vee \  \neg Q)\ \vee \  \neg A)\ \rightarrow \  \neg (D\ \vee \  \neg \neg (\neg Q\ \vee \  \neg A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg Q$ in \hyperref[hilb27:13]{$13$}
} \\
\label{hilb27:15}
  $15$ & $\neg (\neg \neg (\neg P\ \vee \  \neg Q)\ \vee \  \neg A)\ \rightarrow \  \neg (\neg P\ \vee \  \neg \neg (\neg Q\ \vee \  \neg A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $\neg P$ in \hyperref[hilb27:14]{$14$}
} \\
\label{hilb27:16}
  $16$ & $(\neg (\neg P\ \vee \  \neg Q)\ \wedge \  A)\ \rightarrow \  \neg (\neg P\ \vee \  \neg \neg (\neg Q\ \vee \  \neg A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb27:15]{$15$} at occurence $1$
} \\
\label{hilb27:17}
  $17$ & $((P\ \wedge \  Q)\ \wedge \  A)\ \rightarrow \  \neg (\neg P\ \vee \  \neg \neg (\neg Q\ \vee \  \neg A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb27:16]{$16$} at occurence $1$
} \\
\label{hilb27:18}
  $18$ & $((P\ \wedge \  Q)\ \wedge \  A)\ \rightarrow \  (P\ \wedge \  \neg (\neg Q\ \vee \  \neg A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb27:17]{$17$} at occurence $1$
} \\
\label{hilb27:19}
  $19$ & $((P\ \wedge \  Q)\ \wedge \  A)\ \rightarrow \  (P\ \wedge \  (Q\ \wedge \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb27:18]{$18$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Form for the conjunction rule:




\begin{thm}[hilb28]
\hypertarget{hilb28}{}
\begin{displaymath}
P\ \rightarrow \  (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{hilb28:1}
  $1$ & $P\ \vee \  \neg P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb4}{hilb4} } \\
\label{hilb28:2}
  $2$ & $(\neg P\ \vee \  \neg Q)\ \vee \  \neg (\neg P\ \vee \  \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $\neg P\ \vee \  \neg Q$ in \hyperref[hilb28:1]{$1$}
} \\
\label{hilb28:3}
  $3$ & $((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{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb15}{hilb15} } \\
\label{hilb28:4}
  $4$ & $((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[hilb28:3]{$3$}
} \\
\label{hilb28:5}
  $5$ & $((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[hilb28:4]{$4$}
} \\
\label{hilb28:6}
  $6$ & $((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[hilb28:5]{$5$}
} \\
\label{hilb28:7}
  $7$ & $((D\ \vee \  C)\ \vee \  \neg (\neg P\ \vee \  \neg Q))\ \rightarrow \  (D\ \vee \  (C\ \vee \  \neg (\neg P\ \vee \  \neg Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $\neg (\neg P\ \vee \  \neg Q)$ in \hyperref[hilb28:6]{$6$}
} \\
\label{hilb28:8}
  $8$ & $((D\ \vee \  \neg Q)\ \vee \  \neg (\neg P\ \vee \  \neg Q))\ \rightarrow \  (D\ \vee \  (\neg Q\ \vee \  \neg (\neg P\ \vee \  \neg Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $\neg Q$ in \hyperref[hilb28:7]{$7$}
} \\
\label{hilb28:9}
  $9$ & $((\neg P\ \vee \  \neg Q)\ \vee \  \neg (\neg P\ \vee \  \neg Q))\ \rightarrow \  (\neg P\ \vee \  (\neg Q\ \vee \  \neg (\neg P\ \vee \  \neg Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $\neg P$ in \hyperref[hilb28:8]{$8$}
} \\
\label{hilb28:10}
  $10$ & $\neg P\ \vee \  (\neg Q\ \vee \  \neg (\neg P\ \vee \  \neg Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb28:2]{$2$}, \hyperref[hilb28:9]{$9$}} \\
\label{hilb28:11}
  $11$ & $P\ \rightarrow \  (\neg Q\ \vee \  \neg (\neg P\ \vee \  \neg 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[hilb28:10]{$10$} at occurence $1$
} \\
\label{hilb28:12}
  $12$ & $P\ \rightarrow \  (Q\ \rightarrow \  \neg (\neg P\ \vee \  \neg 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[hilb28:11]{$11$} at occurence $1$
} \\
\label{hilb28:13}
  $13$ & $P\ \rightarrow \  (Q\ \rightarrow \  (P\ \wedge \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb28:12]{$12$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Preconditions could be put together in a conjunction (first direction):




\begin{thm}[hilb29]
\hypertarget{hilb29}{}
\begin{displaymath}
(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \wedge \  Q)\ \rightarrow \  A)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb29:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb2}{hilb2} } \\
\label{hilb29:2}
  $2$ & $Q\ \rightarrow \  Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb29:1]{$1$}
} \\
\label{hilb29:3}
  $3$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P\ \rightarrow \  (Q\ \rightarrow \  A)$ in \hyperref[hilb29:2]{$2$}
} \\
\label{hilb29:4}
  $4$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (\neg P\ \vee \  (Q\ \rightarrow \  A))$
  & {\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[hilb29:3]{$3$} at occurence $4$
} \\
\label{hilb29:5}
  $5$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (\neg P\ \vee \  (\neg Q\ \vee \  A))$
  & {\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[hilb29:4]{$4$} at occurence $4$
} \\
\label{hilb29:6}
  $6$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((\neg P\ \vee \  \neg Q)\ \vee \  A)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb29:5]{$5$} at \hyperref[hilb29:1]{$1$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb14}{hilb14}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb14}{hilb14} 
} \\
\label{hilb29:7}
  $7$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (\neg \neg (\neg P\ \vee \  \neg Q)\ \vee \  A)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb29:6]{$6$} at \hyperref[hilb29:8]{$8$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb29:8}
  $8$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (\neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb29:7]{$7$} at occurence $1$
} \\
\label{hilb29:9}
  $9$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \wedge \  Q)\ \rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb29:8]{$8$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Preconditions could be put together in a conjunction (second direction):




\begin{thm}[hilb30]
\hypertarget{hilb30}{}
\begin{displaymath}
((P\ \wedge \  Q)\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb30:1}
  $1$ & $P\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb2}{hilb2} } \\
\label{hilb30:2}
  $2$ & $Q\ \rightarrow \  Q$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb30:1]{$1$}
} \\
\label{hilb30:3}
  $3$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P\ \rightarrow \  (Q\ \rightarrow \  A)$ in \hyperref[hilb30:2]{$2$}
} \\
\label{hilb30:4}
  $4$ & $(\neg P\ \vee \  (Q\ \rightarrow \  A))\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\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[hilb30:3]{$3$} at occurence $2$
} \\
\label{hilb30:5}
  $5$ & $(\neg P\ \vee \  (\neg Q\ \vee \  A))\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\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[hilb30:4]{$4$} at occurence $2$
} \\
\label{hilb30:6}
  $6$ & $((\neg P\ \vee \  \neg Q)\ \vee \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb30:5]{$5$} at \hyperref[hilb30:1]{$1$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb14}{hilb14}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb14}{hilb14} 
} \\
\label{hilb30:7}
  $7$ & $(\neg \neg (\neg P\ \vee \  \neg Q)\ \vee \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb30:6]{$6$} at \hyperref[hilb30:3]{$3$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb5}{hilb5} 
} \\
\label{hilb30:8}
  $8$ & $(\neg (\neg P\ \vee \  \neg Q)\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb30:7]{$7$} at occurence $1$
} \\
\label{hilb30:9}
  $9$ & $((P\ \wedge \  Q)\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb30:8]{$8$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Absorbtion of a conjunction (first direction):




\begin{thm}[hilb31]
\hypertarget{hilb31}{}
\begin{displaymath}
(P\ \wedge \  P)\ \rightarrow \  P\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb31:1}
  $1$ & $(P\ \wedge \  Q)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb24}{hilb24} } \\
\label{hilb31:2}
  $2$ & $(P\ \wedge \  P)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $P$ in \hyperref[hilb31:1]{$1$}
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Absorbtion of a conjunction (second direction):




\begin{thm}[hilb32]
\hypertarget{hilb32}{}
\begin{displaymath}
P\ \rightarrow \  (P\ \wedge \  P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb32:1}
  $1$ & $(P\ \vee \  P)\ \rightarrow \  P$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb11}{hilb11} } \\
\label{hilb32:2}
  $2$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (\neg Q\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb7}{hilb7} } \\
\label{hilb32:3}
  $3$ & $(P\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb32:2]{$2$}
} \\
\label{hilb32:4}
  $4$ & $(B\ \rightarrow \  A)\ \rightarrow \  (\neg A\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb32:3]{$3$}
} \\
\label{hilb32:5}
  $5$ & $(B\ \rightarrow \  P)\ \rightarrow \  (\neg P\ \rightarrow \  \neg B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $P$ in \hyperref[hilb32:4]{$4$}
} \\
\label{hilb32:6}
  $6$ & $((P\ \vee \  P)\ \rightarrow \  P)\ \rightarrow \  (\neg P\ \rightarrow \  \neg (P\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P\ \vee \  P$ in \hyperref[hilb32:5]{$5$}
} \\
\label{hilb32:7}
  $7$ & $\neg P\ \rightarrow \  \neg (P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb32:1]{$1$}, \hyperref[hilb32:6]{$6$}} \\
\label{hilb32:8}
  $8$ & $\neg Q\ \rightarrow \  \neg (Q\ \vee \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb32:7]{$7$}
} \\
\label{hilb32:9}
  $9$ & $\neg \neg P\ \rightarrow \  \neg (\neg P\ \vee \  \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $\neg P$ in \hyperref[hilb32:8]{$8$}
} \\
\label{hilb32:10}
  $10$ & $P\ \rightarrow \  \neg (\neg P\ \vee \  \neg P)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb32:9]{$9$} at \hyperref[hilb32:1]{$1$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb6}{hilb6}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb6}{hilb6} 
} \\
\label{hilb32:11}
  $11$ & $P\ \rightarrow \  (P\ \wedge \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{and}{and} in \hyperref[hilb32:10]{$10$} at occurence $1$
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Absorbtion of identical preconditions (first direction):




\begin{thm}[hilb33]
\hypertarget{hilb33}{}
\begin{displaymath}
(P\ \rightarrow \  (P\ \rightarrow \  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{hilb33:1}
  $1$ & $(P\ \rightarrow \  (Q\ \rightarrow \  A))\ \rightarrow \  ((P\ \wedge \  Q)\ \rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb29}{hilb29} } \\
\label{hilb33:2}
  $2$ & $(P\ \rightarrow \  (Q\ \rightarrow \  B))\ \rightarrow \  ((P\ \wedge \  Q)\ \rightarrow \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb33:1]{$1$}
} \\
\label{hilb33:3}
  $3$ & $(P\ \rightarrow \  (C\ \rightarrow \  B))\ \rightarrow \  ((P\ \wedge \  C)\ \rightarrow \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb33:2]{$2$}
} \\
\label{hilb33:4}
  $4$ & $(D\ \rightarrow \  (C\ \rightarrow \  B))\ \rightarrow \  ((D\ \wedge \  C)\ \rightarrow \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb33:3]{$3$}
} \\
\label{hilb33:5}
  $5$ & $(D\ \rightarrow \  (C\ \rightarrow \  Q))\ \rightarrow \  ((D\ \wedge \  C)\ \rightarrow \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb33:4]{$4$}
} \\
\label{hilb33:6}
  $6$ & $(D\ \rightarrow \  (P\ \rightarrow \  Q))\ \rightarrow \  ((D\ \wedge \  P)\ \rightarrow \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $P$ in \hyperref[hilb33:5]{$5$}
} \\
\label{hilb33:7}
  $7$ & $(P\ \rightarrow \  (P\ \rightarrow \  Q))\ \rightarrow \  ((P\ \wedge \  P)\ \rightarrow \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $P$ in \hyperref[hilb33:6]{$6$}
} \\
\label{hilb33:8}
  $8$ & $(P\ \rightarrow \  (P\ \rightarrow \  Q))\ \rightarrow \  (P\ \rightarrow \  Q)$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb33:7]{$7$} at \hyperref[hilb33:1]{$1$} of \hyperref{}{}{hilb31}{hilb31}  with \hyperref{}{}{hilb31}{hilb31} 
} \\
 & & \qedhere
\end{longtable}
\end{proof}



Absorbtion of identical preconditions (second direction):




\begin{thm}[hilb34]
\hypertarget{hilb34}{}
\begin{displaymath}
(P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  (P\ \rightarrow \  Q))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb34:1}
  $1$ & $((P\ \wedge \  Q)\ \rightarrow \  A)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb30}{hilb30} } \\
\label{hilb34:2}
  $2$ & $((P\ \wedge \  Q)\ \rightarrow \  B)\ \rightarrow \  (P\ \rightarrow \  (Q\ \rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb34:1]{$1$}
} \\
\label{hilb34:3}
  $3$ & $((P\ \wedge \  C)\ \rightarrow \  B)\ \rightarrow \  (P\ \rightarrow \  (C\ \rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb34:2]{$2$}
} \\
\label{hilb34:4}
  $4$ & $((D\ \wedge \  C)\ \rightarrow \  B)\ \rightarrow \  (D\ \rightarrow \  (C\ \rightarrow \  B))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb34:3]{$3$}
} \\
\label{hilb34:5}
  $5$ & $((D\ \wedge \  C)\ \rightarrow \  Q)\ \rightarrow \  (D\ \rightarrow \  (C\ \rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb34:4]{$4$}
} \\
\label{hilb34:6}
  $6$ & $((D\ \wedge \  P)\ \rightarrow \  Q)\ \rightarrow \  (D\ \rightarrow \  (P\ \rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $P$ in \hyperref[hilb34:5]{$5$}
} \\
\label{hilb34:7}
  $7$ & $((P\ \wedge \  P)\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  (P\ \rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $P$ in \hyperref[hilb34:6]{$6$}
} \\
\label{hilb34:8}
  $8$ & $(P\ \rightarrow \  Q)\ \rightarrow \  (P\ \rightarrow \  (P\ \rightarrow \  Q))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb34:7]{$7$} at \hyperref[hilb34:1]{$1$} of \hyperref{}{}{hilb31}{hilb31}  with \hyperref{}{}{hilb31}{hilb31} 
} \\
 & & \qedhere
\end{longtable}
\end{proof}


\section{Cross Reference}

This module is used by the following modules:

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


\end{document}