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

\documentclass{amsart}

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

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

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

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

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

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

\sloppy

\begin{document}

\title{Further Theorems of Propositional Calculus}
\author{Michael Meyling}
\email{principa@meyling.com}
\date{2002-07-27T20:55:58}

\begin{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)
\end{abstract}

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


\section*{module specification}

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


\medskip
This module has the following specification:

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


\medskip
The following modules were used:

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

\medskip
Is used by the following modules:

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



Negation of a conjunction:




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



The reverse of a negation of a conjunction:




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



Negation of a disjunction:




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



Reverse of a negation of a disjunction:




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



The Conjunction is commutative:




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



A technical lemma that is simular to the previous one:




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



Reduction of a conjunction:




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



Another form of a reduction of a conjunction:




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



The conjunction is associative too (first implication):




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



The conjunction is associative (second implication):




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



Form for the conjunction rule:




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



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




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



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




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



Absorbtion of a conjunction (first direction):




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



Absorbtion of a conjunction (second direction):




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



Absorbtion of identical preconditions (first direction):




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



Absorbtion of identical preconditions (second direction):




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

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

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