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

\documentclass{amsart}

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

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

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

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

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

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

\sloppy

\begin{document}

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

\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: & prophilbert1 \\
Version: & 1.00.00 \\
Rule version: & 1.02.00 \\
Orgin: & \url{http://www.meyling.com/principia/0_00_51/prophilbert1_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: & propaxiom \\
Version: & 1.00.00 \\
Rule version: & 1.00.00 \\
Orgin: & \url{propaxiom_1.00.00_1.00.00.qedeq}  \\
pdf: & \url{propaxiom_1.00.00_1.00.00.pdf}  \\
Name: & subst \\
Version: & 1.00.00 \\
Rule version: & 1.01.00 \\
Orgin: & \url{subst_1.00.00_1.01.00.qedeq}  \\
pdf: & \url{subst_1.00.00_1.01.00.pdf}  \\
\end{longtable}

\medskip
Is used by the following modules:

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



\begin{dec}
Apply Axiom
\hypertarget{rule9}{}
\label{rule9}
\end{dec}




\begin{dec}
Apply Sentence
\hypertarget{rule10}{}
\label{rule10}
\end{dec}




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




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


This proposition is the form for the Hypothetical Syllogism.



\bigskip




Now we could declare the rule {\it Hypothetical Syllogism}.
      \par
      parameters: \par
      \begin{tabular}{ll}
      $p$ & proof line number \\
      $m$ & proof line number \\
      \end{tabular}
      \par
      If the proof line $n$ has the form `$(p\ \Rightarrow \ q)$'; and the proof line $m$ has the form `$(q\ \Rightarrow \ r)$'  (p, q and r must be formulas), then the string `$(p\ \Rightarrow \ s)$' could be added as a new proof line.
      \par




\begin{dec}
Hypothetical Syllogism
\hypertarget{rule11}{}
\label{rule11}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{hilb1}{hilb1} 




The self implication could be derived:




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



One form of the classical {\bf tertium non datur}




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



The standard form of the excluded middle:




\begin{thm}
\hypertarget{hilb4}{}
\begin{displaymath}
(P\ \vee \  \neg P)\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb4:1}
  $1$ & $(\neg P\ \vee \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb3}{hilb3} } \\
\label{hilb4:2}
  $2$ & $(P\ \vee \  \neg P)$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} in \hyperref[hilb4:1]{$1$}
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Double negation is implicated:




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



The reverse is also true:




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



The correct reverse of an implication:




\begin{thm}
\hypertarget{hilb7}{}
\begin{displaymath}
((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg Q\ \Rightarrow \  \neg P))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb7:1}
  $1$ & $(P\ \Rightarrow \  \neg \neg P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb5}{hilb5} } \\
\label{hilb7:2}
  $2$ & $(Q\ \Rightarrow \  \neg \neg Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb7:1]{$1$}
} \\
\label{hilb7:3}
  $3$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg P\ \vee \  \neg \neg Q))$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb7:2]{$2$}
} \\
\label{hilb7:4}
  $4$ & $((P\ \vee \  Q)\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\
\label{hilb7:5}
  $5$ & $((\neg P\ \vee \  \neg \neg Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb7:4]{$4$}
} \\
\label{hilb7:6}
  $6$ & $((\neg P\ \vee \  Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb7:3]{$3$} and \hyperref[hilb7:5]{$5$}
} \\
\label{hilb7:7}
  $7$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg \neg Q\ \vee \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb7:6]{$6$} at occurence $1$
} \\
\label{hilb7:8}
  $8$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  (\neg Q\ \Rightarrow \  \neg P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule6}{reverse abbreviation} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{impl}{impl} in \hyperref[hilb7:7]{$7$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



\begin{dec}
Correct reverse of an implication
\hypertarget{rule12}{}
\label{rule12}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{hilb7}{hilb7} 




\begin{dec}
Add a Conjunction on the Left
\hypertarget{rule13}{}
\label{rule13}
\end{dec}


{\it References, needed for declaration:}


\hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} 




\begin{dec}
Add a Conjunction on the Right
\hypertarget{rule14}{}
\label{rule14}
\end{dec}


{\it References, needed for declaration:}


\hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} 
, \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} 




Definition of an Implication 1. part:




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



Definition of an Implication 2. part:




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



\begin{dec}
Addition of an Implication on the Right
\hypertarget{rule17}{}
\label{rule17}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defimpl1}{defimpl1} 
, \hyperref{}{}{defimpl2}{defimpl2} 




\begin{dec}
Addition of an Implication on the Left
\hypertarget{rule18}{}
\label{rule18}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defimpl1}{defimpl1} 
, \hyperref{}{}{defimpl2}{defimpl2} 




Definition of a Conjunction 1. part:




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



Definition of a Conjunction 2. part:




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



\begin{dec}
Addition of a Conjunction on the Left
\hypertarget{rule19}{}
\label{rule19}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defand1}{defand1} 
, \hyperref{}{}{defand2}{defand2} 




\begin{dec}
Addition of a Conjunction on the Right
\hypertarget{rule20}{}
\label{rule20}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defand1}{defand1} 
, \hyperref{}{}{defand2}{defand2} 




Definition of an Equivalence 1. part:




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



Definition of an Equivalence 2. part:




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



\begin{dec}
Addition of an Equivalence on the Left
\hypertarget{rule21}{}
\label{rule21}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defequi1}{defequi1} 
, \hyperref{}{}{defequi2}{defequi2} 




\begin{dec}
Addition of an Equivalence on the Right
\hypertarget{rule22}{}
\label{rule22}
\end{dec}


{\it References, needed for declaration:}


\hyperref{}{}{defequi1}{defequi1} 
, \hyperref{}{}{defequi2}{defequi2} 




\begin{dec}
Elementary equivalence of two formulas
\hypertarget{rule30}{}
\label{rule30}
\end{dec}




A simular formulation for the second axiom:




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



A technical lemma (equal to the third axiom):




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



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




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



A technical lemma (equal to the first axiom):




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



A simple propositon that follows directly from the second axiom:




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



This is a pre form for the associative law:




\begin{thm}
\hypertarget{hilb13}{}
\begin{displaymath}
((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb13:1}
  $1$ & $(P\ \Rightarrow \  (Q\ \vee \  P))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb8}{hilb8} } \\
\label{hilb13:2}
  $2$ & $(A\ \Rightarrow \  (P\ \vee \  A))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb13:1]{$1$}
} \\
\label{hilb13:3}
  $3$ & $((Q\ \vee \  A)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb13:2]{$2$}
} \\
\label{hilb13:4}
  $4$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb13:3]{$3$}
} \\
\label{hilb13:5}
  $5$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  P))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb13:4]{$4$} at \hyperref[hilb13:3]{$3$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb13:6}
  $6$ & $((P\ \vee \  A)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $(P\ \vee \  A)$ in \hyperref[hilb13:1]{$1$}
} \\
\label{hilb13:7}
  $7$ & $(P\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom2}{axiom2} } \\
\label{hilb13:8}
  $8$ & $(P\ \Rightarrow \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb13:7]{$7$}
} \\
\label{hilb13:9}
  $9$ & $(P\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb13:8]{$8$} and \hyperref[hilb13:6]{$6$}
} \\
\label{hilb13:10}
  $10$ & $(((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  ((Q\ \vee \  (P\ \vee \  A))\ \vee \  (Q\ \vee \  (P\ \vee \  A))))$
  & {\tiny \hyperref{}{}{rule9}{apply} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom4}{axiom4} in \hyperref[hilb13:9]{$9$}
} \\
\label{hilb13:11}
  $11$ & $(((Q\ \vee \  (P\ \vee \  A))\ \vee \  P)\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb13:10]{$10$} at \hyperref[hilb13:1]{$1$} of \hyperref{}{}{hilb11}{hilb11}  with \hyperref{}{}{hilb11}{hilb11} 
} \\
\label{hilb13:12}
  $12$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb13:5]{$5$} and \hyperref[hilb13:11]{$11$}
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



The associative law for the disjunction (first direction):




\begin{thm}
\hypertarget{hilb14}{}
\begin{displaymath}
((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb14:1}
  $1$ & $(P\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb2}{hilb2} } \\
\label{hilb14:2}
  $2$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb14:1]{$1$}
} \\
\label{hilb14:3}
  $3$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb14:2]{$2$} at \hyperref[hilb14:4]{$4$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb14:4}
  $4$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (Q\ \vee \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb13}{hilb13} } \\
\label{hilb14:5}
  $5$ & $((P\ \vee \  (A\ \vee \  Q))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb14:4]{$4$}
} \\
\label{hilb14:6}
  $6$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  (A\ \vee \  (P\ \vee \  Q)))$
  & {\tiny \hyperref{}{}{rule11}{HS} with \hyperref[hilb14:3]{$3$} and \hyperref[hilb14:5]{$5$}
} \\
\label{hilb14:7}
  $7$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb14:6]{$6$} at \hyperref[hilb14:3]{$3$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



The associative law for the disjunction (second direction):




\begin{thm}
\hypertarget{hilb15}{}
\begin{displaymath}
(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb15:1}
  $1$ & $((P\ \vee \  (Q\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb14}{hilb14} } \\
\label{hilb15:2}
  $2$ & $((A\ \vee \  (Q\ \vee \  P))\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb15:1]{$1$}
} \\
\label{hilb15:3}
  $3$ & $(((Q\ \vee \  P)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:2]{$2$} at \hyperref[hilb15:1]{$1$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb15:4}
  $4$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  ((A\ \vee \  Q)\ \vee \  P))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:3]{$3$} at \hyperref[hilb15:2]{$2$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb15:5}
  $5$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (A\ \vee \  Q)))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:4]{$4$} at \hyperref[hilb15:3]{$3$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\label{hilb15:6}
  $6$ & $(((P\ \vee \  Q)\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \vee \  A)))$
  & {\tiny \hyperref{}{}{rule30}{elementary equivalence} in \hyperref[hilb15:5]{$5$} at \hyperref[hilb15:4]{$4$} of \hyperref{}{}{hilb9}{hilb9}  with \hyperref{}{}{hilb9}{hilb9} 
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



Another consequence from hilb13 is the exchange of preconditions:




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



An analogus form for \ref{hilb16}:




\begin{thm}
\hypertarget{hilb17}{}
\begin{displaymath}
((Q\ \Rightarrow \  (P\ \Rightarrow \  A))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \Rightarrow \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb17:1}
  $1$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  A))\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \Rightarrow \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{}{}{hilb16}{hilb16} } \\
\label{hilb17:2}
  $2$ & $((Q\ \Rightarrow \  (P\ \Rightarrow \  A))\ \Rightarrow \  (P\ \Rightarrow \  (Q\ \Rightarrow \  A)))$
  & {\tiny \hyperref{subst_1.00.00_1.01.00.pdf}{}{rule8}{Substitute Variables} in \hyperref[hilb17:1]{$1$}
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}

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

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

\end{document}