%%% ====================================================================
%%% @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{prophilbert3_1.00.00_1.02.00.qedeq}
\hyperbaseurl{prophilbert3_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:56:01}

\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: & prophilbert3 \\
Version: & 1.00.00 \\
Rule version: & 1.02.00 \\
Orgin: & \url{http://www.meyling.com/principia/0_00_51/prophilbert3_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: & 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}

\medskip
Is used by the following modules:

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



First distributive law (first direction):




\begin{thm}
\hypertarget{hilb36}{}
\begin{displaymath}
((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb36:1}
  $1$ & $((P\ \wedge \  Q)\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert2_1.00.00_1.02.00.pdf}{}{hilb24}{hilb24} } \\
\label{hilb36:2}
  $2$ & $((P\ \wedge \  A)\ \Rightarrow \  P)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb36:1]{$1$}
} \\
\label{hilb36:3}
  $3$ & $((B\ \wedge \  A)\ \Rightarrow \  B)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb36:2]{$2$}
} \\
\label{hilb36:4}
  $4$ & $((Q\ \wedge \  A)\ \Rightarrow \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb36:3]{$3$}
} \\
\label{hilb36:5}
  $5$ & $((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{hilb36:6}
  $6$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb36:5]{$5$}
} \\
\label{hilb36:7}
  $7$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb36:6]{$6$}
} \\
\label{hilb36:8}
  $8$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  D)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb36:7]{$7$}
} \\
\label{hilb36:9}
  $9$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb36:8]{$8$}
} \\
\label{hilb36:10}
  $10$ & $((D\ \Rightarrow \  Q)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $Q$ in \hyperref[hilb36:9]{$9$}
} \\
\label{hilb36:11}
  $11$ & $(((Q\ \wedge \  A)\ \Rightarrow \  Q)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(Q\ \wedge \  A)$ in \hyperref[hilb36:10]{$10$}
} \\
\label{hilb36:12}
  $12$ & $((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:4]{$4$}, \hyperref[hilb36:11]{$11$}} \\
\label{hilb36:13}
  $13$ & $((P\ \wedge \  Q)\ \Rightarrow \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert2_1.00.00_1.02.00.pdf}{}{hilb25}{hilb25} } \\
\label{hilb36:14}
  $14$ & $((P\ \wedge \  A)\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb36:13]{$13$}
} \\
\label{hilb36:15}
  $15$ & $((B\ \wedge \  A)\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb36:14]{$14$}
} \\
\label{hilb36:16}
  $16$ & $((Q\ \wedge \  A)\ \Rightarrow \  A)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb36:15]{$15$}
} \\
\label{hilb36:17}
  $17$ & $((D\ \Rightarrow \  A)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $A$ in \hyperref[hilb36:9]{$9$}
} \\
\label{hilb36:18}
  $18$ & $(((Q\ \wedge \  A)\ \Rightarrow \  A)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(Q\ \wedge \  A)$ in \hyperref[hilb36:17]{$17$}
} \\
\label{hilb36:19}
  $19$ & $((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:16]{$16$}, \hyperref[hilb36:18]{$18$}} \\
\label{hilb36:20}
  $20$ & $(P\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \wedge \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert2_1.00.00_1.02.00.pdf}{}{hilb28}{hilb28} } \\
\label{hilb36:21}
  $21$ & $(P\ \Rightarrow \  (A\ \Rightarrow \  (P\ \wedge \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb36:20]{$20$}
} \\
\label{hilb36:22}
  $22$ & $(B\ \Rightarrow \  (A\ \Rightarrow \  (B\ \wedge \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb36:21]{$21$}
} \\
\label{hilb36:23}
  $23$ & $(B\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (B\ \wedge \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $(P\ \vee \  A)$ in \hyperref[hilb36:22]{$22$}
} \\
\label{hilb36:24}
  $24$ & $((P\ \vee \  Q)\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  Q)$ in \hyperref[hilb36:23]{$23$}
} \\
\label{hilb36:25}
  $25$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb1}{hilb1} } \\
\label{hilb36:26}
  $26$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb36:25]{$25$}
} \\
\label{hilb36:27}
  $27$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb36:26]{$26$}
} \\
\label{hilb36:28}
  $28$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb36:27]{$27$}
} \\
\label{hilb36:29}
  $29$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \wedge \  A))$ in \hyperref[hilb36:28]{$28$}
} \\
\label{hilb36:30}
  $30$ & $((D\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  (((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))$ in \hyperref[hilb36:29]{$29$}
} \\
\label{hilb36:31}
  $31$ & $(((P\ \vee \  Q)\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  (((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  Q))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  Q)$ in \hyperref[hilb36:30]{$30$}
} \\
\label{hilb36:32}
  $32$ & $(((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  Q))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:24]{$24$}, \hyperref[hilb36:31]{$31$}} \\
\label{hilb36:33}
  $33$ & $((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:12]{$12$}, \hyperref[hilb36:32]{$32$}} \\
\label{hilb36:34}
  $34$ & $((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{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb16}{hilb16} } \\
\label{hilb36:35}
  $35$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  B))\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb36:34]{$34$}
} \\
\label{hilb36:36}
  $36$ & $((P\ \Rightarrow \  (C\ \Rightarrow \  B))\ \Rightarrow \  (C\ \Rightarrow \  (P\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb36:35]{$35$}
} \\
\label{hilb36:37}
  $37$ & $((D\ \Rightarrow \  (C\ \Rightarrow \  B))\ \Rightarrow \  (C\ \Rightarrow \  (D\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb36:36]{$36$}
} \\
\label{hilb36:38}
  $38$ & $((D\ \Rightarrow \  (C\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  (C\ \Rightarrow \  (D\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))$ in \hyperref[hilb36:37]{$37$}
} \\
\label{hilb36:39}
  $39$ & $((D\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (D\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  A)$ in \hyperref[hilb36:38]{$38$}
} \\
\label{hilb36:40}
  $40$ & $(((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  (Q\ \wedge \  A))$ in \hyperref[hilb36:39]{$39$}
} \\
\label{hilb36:41}
  $41$ & $((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:33]{$33$}, \hyperref[hilb36:40]{$40$}} \\
\label{hilb36:42}
  $42$ & $((D\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  (((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))$ in \hyperref[hilb36:29]{$29$}
} \\
\label{hilb36:43}
  $43$ & $(((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  (((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  A)$ in \hyperref[hilb36:42]{$42$}
} \\
\label{hilb36:44}
  $44$ & $(((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  (P\ \vee \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:41]{$41$}, \hyperref[hilb36:43]{$43$}} \\
\label{hilb36:45}
  $45$ & $((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:19]{$19$}, \hyperref[hilb36:44]{$44$}} \\
\label{hilb36:46}
  $46$ & $((P\ \Rightarrow \  (P\ \Rightarrow \  Q))\ \Rightarrow \  (P\ \Rightarrow \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert2_1.00.00_1.02.00.pdf}{}{hilb33}{hilb33} } \\
\label{hilb36:47}
  $47$ & $((P\ \Rightarrow \  (P\ \Rightarrow \  A))\ \Rightarrow \  (P\ \Rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb36:46]{$46$}
} \\
\label{hilb36:48}
  $48$ & $((B\ \Rightarrow \  (B\ \Rightarrow \  A))\ \Rightarrow \  (B\ \Rightarrow \  A))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb36:47]{$47$}
} \\
\label{hilb36:49}
  $49$ & $((B\ \Rightarrow \  (B\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  (B\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))$ in \hyperref[hilb36:48]{$48$}
} \\
\label{hilb36:50}
  $50$ & $(((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))\ \Rightarrow \  ((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \wedge \  A))$ in \hyperref[hilb36:49]{$49$}
} \\
\label{hilb36:51}
  $51$ & $((P\ \vee \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb36:45]{$45$}, \hyperref[hilb36:50]{$50$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



First distributive law (second direction):




\begin{thm}
\hypertarget{hilb37}{}
\begin{displaymath}
(((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))\end{displaymath}
\end{thm}
\begin{proof}
\mbox{}\\
\begin{longtable}[h!]{r@{\extracolsep{\fill}}p{9cm}@{\extracolsep{\fill}}p{4cm}}
\label{hilb37:1}
  $1$ & $(P\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \wedge \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert2_1.00.00_1.02.00.pdf}{}{hilb28}{hilb28} } \\
\label{hilb37:2}
  $2$ & $(P\ \Rightarrow \  (A\ \Rightarrow \  (P\ \wedge \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $A$ in \hyperref[hilb37:1]{$1$}
} \\
\label{hilb37:3}
  $3$ & $(B\ \Rightarrow \  (A\ \Rightarrow \  (B\ \wedge \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $B$ in \hyperref[hilb37:2]{$2$}
} \\
\label{hilb37:4}
  $4$ & $(Q\ \Rightarrow \  (A\ \Rightarrow \  (Q\ \wedge \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb37:3]{$3$}
} \\
\label{hilb37:5}
  $5$ & $((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{hilb37:6}
  $6$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb37:5]{$5$}
} \\
\label{hilb37:7}
  $7$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  P)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb37:6]{$6$}
} \\
\label{hilb37:8}
  $8$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \vee \  D)\ \Rightarrow \  (B\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb37:7]{$7$}
} \\
\label{hilb37:9}
  $9$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $P$ in \hyperref[hilb37:8]{$8$}
} \\
\label{hilb37:10}
  $10$ & $((D\ \Rightarrow \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(Q\ \wedge \  A)$ in \hyperref[hilb37:9]{$9$}
} \\
\label{hilb37:11}
  $11$ & $((A\ \Rightarrow \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $A$ in \hyperref[hilb37:10]{$10$}
} \\
\label{hilb37:12}
  $12$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((A\ \Rightarrow \  P)\ \Rightarrow \  (A\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb1}{hilb1} } \\
\label{hilb37:13}
  $13$ & $((P\ \Rightarrow \  Q)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  Q)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb37:12]{$12$}
} \\
\label{hilb37:14}
  $14$ & $((P\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  P)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb37:13]{$13$}
} \\
\label{hilb37:15}
  $15$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((B\ \Rightarrow \  D)\ \Rightarrow \  (B\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb37:14]{$14$}
} \\
\label{hilb37:16}
  $16$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  ((Q\ \Rightarrow \  D)\ \Rightarrow \  (Q\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $Q$ in \hyperref[hilb37:15]{$15$}
} \\
\label{hilb37:17}
  $17$ & $((D\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((Q\ \Rightarrow \  D)\ \Rightarrow \  (Q\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))$ in \hyperref[hilb37:16]{$16$}
} \\
\label{hilb37:18}
  $18$ & $(((A\ \Rightarrow \  (Q\ \wedge \  A))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((Q\ \Rightarrow \  (A\ \Rightarrow \  (Q\ \wedge \  A)))\ \Rightarrow \  (Q\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(A\ \Rightarrow \  (Q\ \wedge \  A))$ in \hyperref[hilb37:17]{$17$}
} \\
\label{hilb37:19}
  $19$ & $((Q\ \Rightarrow \  (A\ \Rightarrow \  (Q\ \wedge \  A)))\ \Rightarrow \  (Q\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:11]{$11$}, \hyperref[hilb37:18]{$18$}} \\
\label{hilb37:20}
  $20$ & $(Q\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:4]{$4$}, \hyperref[hilb37:19]{$19$}} \\
\label{hilb37:21}
  $21$ & $((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{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb16}{hilb16} } \\
\label{hilb37:22}
  $22$ & $((P\ \Rightarrow \  (Q\ \Rightarrow \  B))\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $A$ by $B$ in \hyperref[hilb37:21]{$21$}
} \\
\label{hilb37:23}
  $23$ & $((P\ \Rightarrow \  (C\ \Rightarrow \  B))\ \Rightarrow \  (C\ \Rightarrow \  (P\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $C$ in \hyperref[hilb37:22]{$22$}
} \\
\label{hilb37:24}
  $24$ & $((D\ \Rightarrow \  (C\ \Rightarrow \  B))\ \Rightarrow \  (C\ \Rightarrow \  (D\ \Rightarrow \  B)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $D$ in \hyperref[hilb37:23]{$23$}
} \\
\label{hilb37:25}
  $25$ & $((D\ \Rightarrow \  (C\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  (C\ \Rightarrow \  (D\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \wedge \  A))$ in \hyperref[hilb37:24]{$24$}
} \\
\label{hilb37:26}
  $26$ & $((D\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (D\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  A)$ in \hyperref[hilb37:25]{$25$}
} \\
\label{hilb37:27}
  $27$ & $((Q\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $Q$ in \hyperref[hilb37:26]{$26$}
} \\
\label{hilb37:28}
  $28$ & $((P\ \vee \  A)\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:20]{$20$}, \hyperref[hilb37:27]{$27$}} \\
\label{hilb37:29}
  $29$ & $((D\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))\ \Rightarrow \  ((P\ \vee \  D)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  (Q\ \wedge \  A))$ in \hyperref[hilb37:9]{$9$}
} \\
\label{hilb37:30}
  $30$ & $((Q\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $Q$ in \hyperref[hilb37:29]{$29$}
} \\
\label{hilb37:31}
  $31$ & $((D\ \Rightarrow \  C)\ \Rightarrow \  (((P\ \vee \  A)\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  C)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  A)$ in \hyperref[hilb37:15]{$15$}
} \\
\label{hilb37:32}
  $32$ & $((D\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A)))))\ \Rightarrow \  (((P\ \vee \  A)\ \Rightarrow \  D)\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A)))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A))))$ in \hyperref[hilb37:31]{$31$}
} \\
\label{hilb37:33}
  $33$ & $(((Q\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A)))))\ \Rightarrow \  (((P\ \vee \  A)\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A)))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(Q\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))$ in \hyperref[hilb37:32]{$32$}
} \\
\label{hilb37:34}
  $34$ & $(((P\ \vee \  A)\ \Rightarrow \  (Q\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A))))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:30]{$30$}, \hyperref[hilb37:33]{$33$}} \\
\label{hilb37:35}
  $35$ & $((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:28]{$28$}, \hyperref[hilb37:34]{$34$}} \\
\label{hilb37:36}
  $36$ & $((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  ((P\ \vee \  P)\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb37:35]{$35$} at \hyperref[hilb37: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{hilb37:37}
  $37$ & $((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb37:36]{$36$} at \hyperref[hilb37:1]{$1$} of \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb11}{hilb11}  with \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{hilb11}{hilb11} 
} \\
\label{hilb37:38}
  $38$ & $((D\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (D\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  Q)$ in \hyperref[hilb37:25]{$25$}
} \\
\label{hilb37:39}
  $39$ & $(((P\ \vee \  A)\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((P\ \vee \  Q)\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  A)$ in \hyperref[hilb37:38]{$38$}
} \\
\label{hilb37:40}
  $40$ & $((P\ \vee \  Q)\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:37]{$37$}, \hyperref[hilb37:39]{$39$}} \\
\label{hilb37:41}
  $41$ & $((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{prophilbert2_1.00.00_1.02.00.pdf}{}{hilb29}{hilb29} } \\
\label{hilb37:42}
  $42$ & $((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[hilb37:41]{$41$}
} \\
\label{hilb37:43}
  $43$ & $((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[hilb37:42]{$42$}
} \\
\label{hilb37:44}
  $44$ & $((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[hilb37:43]{$43$}
} \\
\label{hilb37:45}
  $45$ & $((D\ \Rightarrow \  (C\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((D\ \wedge \  C)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $B$ by $(P\ \vee \  (Q\ \wedge \  A))$ in \hyperref[hilb37:44]{$44$}
} \\
\label{hilb37:46}
  $46$ & $((D\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  ((D\ \wedge \  (P\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $C$ by $(P\ \vee \  A)$ in \hyperref[hilb37:45]{$45$}
} \\
\label{hilb37:47}
  $47$ & $(((P\ \vee \  Q)\ \Rightarrow \  ((P\ \vee \  A)\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))\ \Rightarrow \  (((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A))))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $D$ by $(P\ \vee \  Q)$ in \hyperref[hilb37:46]{$46$}
} \\
\label{hilb37:48}
  $48$ & $(((P\ \vee \  Q)\ \wedge \  (P\ \vee \  A))\ \Rightarrow \  (P\ \vee \  (Q\ \wedge \  A)))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:40]{$40$}, \hyperref[hilb37:47]{$47$}} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



A form for the abbreviation rule form for disjunction (first direction):




\begin{thm}
\hypertarget{hilb38}{}
\begin{displaymath}
((P\ \vee \  Q)\ \Rightarrow \  \neg (\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{hilb38: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{hilb38:2}
  $2$ & $(Q\ \Rightarrow \  Q)$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $P$ by $Q$ in \hyperref[hilb38:1]{$1$}
} \\
\label{hilb38:3}
  $3$ & $((P\ \vee \  Q)\ \Rightarrow \  (P\ \vee \  Q))$
  & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace}  $Q$ by $(P\ \vee \  Q)$ in \hyperref[hilb38:2]{$2$}
} \\
\label{hilb38:4}
  $4$ & $((P\ \vee \  Q)\ \Rightarrow \  \neg \neg (P\ \vee \  Q))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb38:3]{$3$} at \hyperref[hilb38: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{hilb38:5}
  $5$ & $((P\ \vee \  Q)\ \Rightarrow \  \neg \neg (\neg \neg P\ \vee \  Q))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb38:4]{$4$} at \hyperref[hilb38: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{hilb38:6}
  $6$ & $((P\ \vee \  Q)\ \Rightarrow \  \neg \neg (\neg \neg P\ \vee \  \neg \neg Q))$
  & {\tiny \hyperref{prophilbert1_1.00.00_1.02.00.pdf}{}{rule30}{elementary equivalence} in \hyperref[hilb38:5]{$5$} at \hyperref[hilb38: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{hilb38:7}
  $7$ & $((P\ \vee \  Q)\ \Rightarrow \  \neg (\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[hilb38:6]{$6$} at occurence $1$
} \\
\\ & & & \mbox{\qedhere}
\end{longtable}
\end{proof}



A form for the abbreviation rule form for disjunction (second direction):




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



By duality we get the second distributive law (first direction):




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



The second distributive law (second direction):




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

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

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

\end{document}