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

\documentclass[a4paper]{article}

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

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


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

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

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

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

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


\begin{document}

\maketitle

\setlongtables



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


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


\section*{Abstract}

This module includes proofs of popositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)


\section*{Specification}

This document has the following specification:

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

\medskip

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




\section*{References}

This document uses the results of the following documents:

\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & 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}


\section*{Content}




First distributive law (first direction):




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



First distributive law (second direction):




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



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




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



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




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



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




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



The second distributive law (second direction):




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


\section{Cross Reference}

This module is used by the following modules:

\begin{longtable}[h!]{l@{\extracolsep{\fill}}p{12cm}}
Name: & 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}