% -*- 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.00.00.qedeq} \hyperbaseurl{prophilbert3_1.00.00_1.00.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 } \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.00.00 \\ Orgin: & \url{http://www.qedeq.org/0_00_53/prophilbert3_1.00.00_1.00.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.00.00 \\ Orgin: & \url{prophilbert2_1.00.00_1.00.00.qedeq} \\ pdf: & \url{prophilbert2_1.00.00_1.00.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.00.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.00.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.00.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.00.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.00.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.00.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.00.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.00.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.00.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 \ (Q\ \vee \ A))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb14}{hilb14} } \\ \label{hilb37:37} $37$ & $(P\ \vee \ (Q\ \vee \ B))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $B$ in \hyperref[hilb37:36]{$36$} } \\ \label{hilb37:38} $38$ & $(P\ \vee \ (C\ \vee \ B))\ \rightarrow \ ((P\ \vee \ C)\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $C$ in \hyperref[hilb37:37]{$37$} } \\ \label{hilb37:39} $39$ & $(D\ \vee \ (C\ \vee \ B))\ \rightarrow \ ((D\ \vee \ C)\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $D$ in \hyperref[hilb37:38]{$38$} } \\ \label{hilb37:40} $40$ & $(D\ \vee \ (C\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((D\ \vee \ C)\ \vee \ (Q\ \wedge \ A))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q\ \wedge \ A$ in \hyperref[hilb37:39]{$39$} } \\ \label{hilb37:41} $41$ & $(D\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((D\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $P$ in \hyperref[hilb37:40]{$40$} } \\ \label{hilb37:42} $42$ & $(P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $P$ in \hyperref[hilb37:41]{$41$} } \\ \label{hilb37:43} $43$ & $(P\ \rightarrow \ Q)\ \rightarrow \ (\neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl1}{defimpl1} } \\ \label{hilb37:44} $44$ & $(\neg P\ \vee \ Q)\ \rightarrow \ (P\ \rightarrow \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl2}{defimpl2} } \\ \label{hilb37:45} $45$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg (P\ \vee \ Q)$ in \hyperref[hilb37:8]{$8$} } \\ \label{hilb37:46} $46$ & $(D\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $(P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)$ in \hyperref[hilb37:45]{$45$} } \\ \label{hilb37:47} $47$ & $((P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:46]{$46$} } \\ \label{hilb37:48} $48$ & $(\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:42]{$42$}, \hyperref[hilb37:47]{$47$}} \\ \label{hilb37:49} $49$ & $(P\ \rightarrow \ B)\ \rightarrow \ (\neg P\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $B$ in \hyperref[hilb37:43]{$43$} } \\ \label{hilb37:50} $50$ & $(C\ \rightarrow \ B)\ \rightarrow \ (\neg C\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $C$ in \hyperref[hilb37:49]{$49$} } \\ \label{hilb37:51} $51$ & $(C\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg C\ \vee \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:50]{$50$} } \\ \label{hilb37:52} $52$ & $((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (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:51]{$51$} } \\ \label{hilb37:53} $53$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:15]{$15$} } \\ \label{hilb37:54} $54$ & $(D\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:53]{$53$} } \\ \label{hilb37:55} $55$ & $((\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:54]{$54$} } \\ \label{hilb37:56} $56$ & $(((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:48]{$48$}, \hyperref[hilb37:55]{$55$}} \\ \label{hilb37:57} $57$ & $((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:52]{$52$}, \hyperref[hilb37:56]{$56$}} \\ \label{hilb37:58} $58$ & $(\neg P\ \vee \ B)\ \rightarrow \ (P\ \rightarrow \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $B$ in \hyperref[hilb37:44]{$44$} } \\ \label{hilb37:59} $59$ & $(\neg C\ \vee \ B)\ \rightarrow \ (C\ \rightarrow \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $C$ in \hyperref[hilb37:58]{$58$} } \\ \label{hilb37:60} $60$ & $(\neg C\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (C\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)$ in \hyperref[hilb37:59]{$59$} } \\ \label{hilb37:61} $61$ & $(\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ 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} $C$ by $P\ \vee \ Q$ in \hyperref[hilb37:60]{$60$} } \\ \label{hilb37:62} $62$ & $(D\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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} $C$ by $(P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:53]{$53$} } \\ \label{hilb37:63} $63$ & $((\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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 $\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:62]{$62$} } \\ \label{hilb37:64} $64$ & $(((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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}{}{rule1}{MP} with \hyperref[hilb37:61]{$61$}, \hyperref[hilb37:63]{$63$}} \\ \label{hilb37:65} $65$ & $((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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}{}{rule1}{MP} with \hyperref[hilb37:57]{$57$}, \hyperref[hilb37:64]{$64$}} \\ \label{hilb37:66} $66$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((\neg (P\ \vee \ A)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg (P\ \vee \ A)$ in \hyperref[hilb37:8]{$8$} } \\ \label{hilb37:67} $67$ & $(D\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((\neg (P\ \vee \ A)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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:66]{$66$} } \\ \label{hilb37:68} $68$ & $(((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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 $(P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:67]{$67$} } \\ \label{hilb37:69} $69$ & $(\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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:65]{$65$}, \hyperref[hilb37:68]{$68$}} \\ \label{hilb37:70} $70$ & $(C\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg C\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:50]{$50$} } \\ \label{hilb37:71} $71$ & $((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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 \ A$ in \hyperref[hilb37:70]{$70$} } \\ \label{hilb37:72} $72$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))$ in \hyperref[hilb37:15]{$15$} } \\ \label{hilb37:73} $73$ & $(D\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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 $\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:72]{$72$} } \\ \label{hilb37:74} $74$ & $((\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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 $\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))$ in \hyperref[hilb37:73]{$73$} } \\ \label{hilb37:75} $75$ & $(((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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:69]{$69$}, \hyperref[hilb37:74]{$74$}} \\ \label{hilb37:76} $76$ & $((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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:71]{$71$}, \hyperref[hilb37:75]{$75$}} \\ \label{hilb37:77} $77$ & $(\neg C\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (C\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:59]{$59$} } \\ \label{hilb37:78} $78$ & $(\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ 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} $C$ by $P\ \vee \ A$ in \hyperref[hilb37:77]{$77$} } \\ \label{hilb37:79} $79$ & $(D\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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} $C$ by $(P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:72]{$72$} } \\ \label{hilb37:80} $80$ & $((\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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 $\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:79]{$79$} } \\ \label{hilb37:81} $81$ & $(((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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:78]{$78$}, \hyperref[hilb37:80]{$80$}} \\ \label{hilb37:82} $82$ & $((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (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:76]{$76$}, \hyperref[hilb37:81]{$81$}} \\ \label{hilb37:83} $83$ & $(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:35]{$35$}, \hyperref[hilb37:82]{$82$}} \\ \label{hilb37:84} $84$ & $(P\ \vee \ P)\ \rightarrow \ P$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb11}{hilb11} } \\ \label{hilb37:85} $85$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((Q\ \wedge \ A)\ \vee \ D)\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q\ \wedge \ A$ in \hyperref[hilb37:8]{$8$} } \\ \label{hilb37:86} $86$ & $(D\ \rightarrow \ P)\ \rightarrow \ (((Q\ \wedge \ A)\ \vee \ D)\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ P))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $P$ in \hyperref[hilb37:85]{$85$} } \\ \label{hilb37:87} $87$ & $((P\ \vee \ P)\ \rightarrow \ P)\ \rightarrow \ (((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ P))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $P\ \vee \ P$ in \hyperref[hilb37:86]{$86$} } \\ \label{hilb37:88} $88$ & $((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:84]{$84$}, \hyperref[hilb37:87]{$87$}} \\ \label{hilb37:89} $89$ & $(P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\ \label{hilb37:90} $90$ & $(P\ \vee \ B)\ \rightarrow \ (B\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $B$ in \hyperref[hilb37:89]{$89$} } \\ \label{hilb37:91} $91$ & $(C\ \vee \ B)\ \rightarrow \ (B\ \vee \ C)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $C$ in \hyperref[hilb37:90]{$90$} } \\ \label{hilb37:92} $92$ & $(C\ \vee \ P)\ \rightarrow \ (P\ \vee \ C)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P$ in \hyperref[hilb37:91]{$91$} } \\ \label{hilb37:93} $93$ & $((Q\ \wedge \ A)\ \vee \ P)\ \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:92]{$92$} } \\ \label{hilb37:94} $94$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ D)\ \rightarrow \ (((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(Q\ \wedge \ A)\ \vee \ (P\ \vee \ P)$ in \hyperref[hilb37:15]{$15$} } \\ \label{hilb37:95} $95$ & $(D\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ D)\ \rightarrow \ (((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ (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:94]{$94$} } \\ \label{hilb37:96} $96$ & $(((Q\ \wedge \ A)\ \vee \ P)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ P))\ \rightarrow \ (((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(Q\ \wedge \ A)\ \vee \ P$ in \hyperref[hilb37:95]{$95$} } \\ \label{hilb37:97} $97$ & $(((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ P))\ \rightarrow \ (((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:93]{$93$}, \hyperref[hilb37:96]{$96$}} \\ \label{hilb37:98} $98$ & $((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:88]{$88$}, \hyperref[hilb37:97]{$97$}} \\ \label{hilb37:99} $99$ & $(C\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ C)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q\ \wedge \ A$ in \hyperref[hilb37:91]{$91$} } \\ \label{hilb37:100} $100$ & $((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $P\ \vee \ P$ in \hyperref[hilb37:99]{$99$} } \\ \label{hilb37:101} $101$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)$ in \hyperref[hilb37:15]{$15$} } \\ \label{hilb37:102} $102$ & $(D\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ (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:101]{$101$} } \\ \label{hilb37:103} $103$ & $(((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P)))\ \rightarrow \ (((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(Q\ \wedge \ A)\ \vee \ (P\ \vee \ P)$ in \hyperref[hilb37:102]{$102$} } \\ \label{hilb37:104} $104$ & $(((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ ((Q\ \wedge \ A)\ \vee \ (P\ \vee \ P)))\ \rightarrow \ (((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:98]{$98$}, \hyperref[hilb37:103]{$103$}} \\ \label{hilb37:105} $105$ & $((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:100]{$100$}, \hyperref[hilb37:104]{$104$}} \\ \label{hilb37:106} $106$ & $(D\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ Q)\ \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:45]{$45$} } \\ \label{hilb37:107} $107$ & $(((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)$ in \hyperref[hilb37:106]{$106$} } \\ \label{hilb37:108} $108$ & $(\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:105]{$105$}, \hyperref[hilb37:107]{$107$}} \\ \label{hilb37:109} $109$ & $(C\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg C\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)$ in \hyperref[hilb37:50]{$50$} } \\ \label{hilb37:110} $110$ & $((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ 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:109]{$109$} } \\ \label{hilb37:111} $111$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:15]{$15$} } \\ \label{hilb37:112} $112$ & $(D\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:111]{$111$} } \\ \label{hilb37:113} $113$ & $((\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:112]{$112$} } \\ \label{hilb37:114} $114$ & $(((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:108]{$108$}, \hyperref[hilb37:113]{$113$}} \\ \label{hilb37:115} $115$ & $((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:110]{$110$}, \hyperref[hilb37:114]{$114$}} \\ \label{hilb37:116} $116$ & $(\neg C\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (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:59]{$59$} } \\ \label{hilb37:117} $117$ & $(\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \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:116]{$116$} } \\ \label{hilb37:118} $118$ & $(D\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (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 \ (Q\ \wedge \ A))$ in \hyperref[hilb37:111]{$111$} } \\ \label{hilb37:119} $119$ & $((\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:118]{$118$} } \\ \label{hilb37:120} $120$ & $(((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:117]{$117$}, \hyperref[hilb37:119]{$119$}} \\ \label{hilb37:121} $121$ & $((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:115]{$115$}, \hyperref[hilb37:120]{$120$}} \\ \label{hilb37:122} $122$ & $(D\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((\neg (P\ \vee \ A)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (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 \ (Q\ \wedge \ A))$ in \hyperref[hilb37:66]{$66$} } \\ \label{hilb37:123} $123$ & $(((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:122]{$122$} } \\ \label{hilb37:124} $124$ & $(\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:121]{$121$}, \hyperref[hilb37:123]{$123$}} \\ \label{hilb37:125} $125$ & $(C\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg C\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:50]{$50$} } \\ \label{hilb37:126} $126$ & $((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((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 \ A$ in \hyperref[hilb37:125]{$125$} } \\ \label{hilb37:127} $127$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:15]{$15$} } \\ \label{hilb37:128} $128$ & $(D\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:127]{$127$} } \\ \label{hilb37:129} $129$ & $((\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:128]{$128$} } \\ \label{hilb37:130} $130$ & $(((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:124]{$124$}, \hyperref[hilb37:129]{$129$}} \\ \label{hilb37:131} $131$ & $((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:126]{$126$}, \hyperref[hilb37:130]{$130$}} \\ \label{hilb37:132} $132$ & $(\neg C\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (C\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))$ in \hyperref[hilb37:59]{$59$} } \\ \label{hilb37:133} $133$ & $(\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \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:132]{$132$} } \\ \label{hilb37:134} $134$ & $(D\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \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)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:127]{$127$} } \\ \label{hilb37:135} $135$ & $((\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ ((((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))$ in \hyperref[hilb37:134]{$134$} } \\ \label{hilb37:136} $136$ & $(((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ (\neg (P\ \vee \ A)\ \vee \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))\ \rightarrow \ (((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:133]{$133$}, \hyperref[hilb37:135]{$135$}} \\ \label{hilb37:137} $137$ & $((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ ((P\ \vee \ P)\ \vee \ (Q\ \wedge \ A))))\ \rightarrow \ ((P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:131]{$131$}, \hyperref[hilb37:136]{$136$}} \\ \label{hilb37:138} $138$ & $(P\ \vee \ A)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ (Q\ \wedge \ A)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb37:83]{$83$}, \hyperref[hilb37:137]{$137$}} \\ \label{hilb37:139} $139$ & $(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:140} $140$ & $((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:139]{$139$} } \\ \label{hilb37:141} $141$ & $(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:138]{$138$}, \hyperref[hilb37:140]{$140$}} \\ \label{hilb37:142} $142$ & $(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.00.00.pdf}{}{hilb29}{hilb29} } \\ \label{hilb37:143} $143$ & $(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:142]{$142$} } \\ \label{hilb37:144} $144$ & $(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:143]{$143$} } \\ \label{hilb37:145} $145$ & $(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:144]{$144$} } \\ \label{hilb37:146} $146$ & $(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:145]{$145$} } \\ \label{hilb37:147} $147$ & $(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:146]{$146$} } \\ \label{hilb37:148} $148$ & $((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:147]{$147$} } \\ \label{hilb37:149} $149$ & $((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:141]{$141$}, \hyperref[hilb37:148]{$148$}} \\ & & \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 \ \neg \neg P$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb5}{hilb5} } \\ \label{hilb38:2} $2$ & $A\ \rightarrow \ \neg \neg A$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $A$ in \hyperref[hilb38:1]{$1$} } \\ \label{hilb38:3} $3$ & $(P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P\ \vee \ Q$ in \hyperref[hilb38:2]{$2$} } \\ \label{hilb38:4} $4$ & $(P\ \rightarrow \ Q)\ \rightarrow \ (\neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl1}{defimpl1} } \\ \label{hilb38:5} $5$ & $(\neg P\ \vee \ Q)\ \rightarrow \ (P\ \rightarrow \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl2}{defimpl2} } \\ \label{hilb38:6} $6$ & $(P\ \rightarrow \ A)\ \rightarrow \ (\neg P\ \vee \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $A$ in \hyperref[hilb38:4]{$4$} } \\ \label{hilb38:7} $7$ & $(B\ \rightarrow \ A)\ \rightarrow \ (\neg B\ \vee \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[hilb38:6]{$6$} } \\ \label{hilb38:8} $8$ & $(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.00.00.pdf}{}{hilb1}{hilb1} } \\ \label{hilb38:9} $9$ & $(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[hilb38:8]{$8$} } \\ \label{hilb38:10} $10$ & $(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[hilb38:9]{$9$} } \\ \label{hilb38:11} $11$ & $(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[hilb38:10]{$10$} } \\ \label{hilb38:12} $12$ & $(\neg P\ \vee \ A)\ \rightarrow \ (P\ \rightarrow \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $A$ in \hyperref[hilb38:5]{$5$} } \\ \label{hilb38:13} $13$ & $(\neg B\ \vee \ A)\ \rightarrow \ (B\ \rightarrow \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[hilb38:12]{$12$} } \\ \label{hilb38:14} $14$ & $Q\ \rightarrow \ \neg \neg Q$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $Q$ in \hyperref[hilb38:1]{$1$} } \\ \label{hilb38:15} $15$ & $(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{hilb38:16} $16$ & $(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[hilb38:15]{$15$} } \\ \label{hilb38:17} $17$ & $(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[hilb38:16]{$16$} } \\ \label{hilb38:18} $18$ & $(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[hilb38:17]{$17$} } \\ \label{hilb38:19} $19$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((Q\ \vee \ D)\ \rightarrow \ (Q\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q$ in \hyperref[hilb38:18]{$18$} } \\ \label{hilb38:20} $20$ & $(D\ \rightarrow \ \neg \neg P)\ \rightarrow \ ((Q\ \vee \ D)\ \rightarrow \ (Q\ \vee \ \neg \neg P))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg P$ in \hyperref[hilb38:19]{$19$} } \\ \label{hilb38:21} $21$ & $(P\ \rightarrow \ \neg \neg P)\ \rightarrow \ ((Q\ \vee \ P)\ \rightarrow \ (Q\ \vee \ \neg \neg P))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $P$ in \hyperref[hilb38:20]{$20$} } \\ \label{hilb38:22} $22$ & $(Q\ \vee \ P)\ \rightarrow \ (Q\ \vee \ \neg \neg P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:1]{$1$}, \hyperref[hilb38:21]{$21$}} \\ \label{hilb38:23} $23$ & $(P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\ \label{hilb38:24} $24$ & $(P\ \vee \ A)\ \rightarrow \ (A\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $A$ in \hyperref[hilb38:23]{$23$} } \\ \label{hilb38:25} $25$ & $(B\ \vee \ A)\ \rightarrow \ (A\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[hilb38:24]{$24$} } \\ \label{hilb38:26} $26$ & $(B\ \vee \ \neg \neg P)\ \rightarrow \ (\neg \neg P\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg P$ in \hyperref[hilb38:25]{$25$} } \\ \label{hilb38:27} $27$ & $(Q\ \vee \ \neg \neg P)\ \rightarrow \ (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q$ in \hyperref[hilb38:26]{$26$} } \\ \label{hilb38:28} $28$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((Q\ \vee \ P)\ \rightarrow \ D)\ \rightarrow \ ((Q\ \vee \ P)\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q\ \vee \ P$ in \hyperref[hilb38:11]{$11$} } \\ \label{hilb38:29} $29$ & $(D\ \rightarrow \ (\neg \neg P\ \vee \ Q))\ \rightarrow \ (((Q\ \vee \ P)\ \rightarrow \ D)\ \rightarrow \ ((Q\ \vee \ P)\ \rightarrow \ (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg P\ \vee \ Q$ in \hyperref[hilb38:28]{$28$} } \\ \label{hilb38:30} $30$ & $((Q\ \vee \ \neg \neg P)\ \rightarrow \ (\neg \neg P\ \vee \ Q))\ \rightarrow \ (((Q\ \vee \ P)\ \rightarrow \ (Q\ \vee \ \neg \neg P))\ \rightarrow \ ((Q\ \vee \ P)\ \rightarrow \ (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $Q\ \vee \ \neg \neg P$ in \hyperref[hilb38:29]{$29$} } \\ \label{hilb38:31} $31$ & $((Q\ \vee \ P)\ \rightarrow \ (Q\ \vee \ \neg \neg P))\ \rightarrow \ ((Q\ \vee \ P)\ \rightarrow \ (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:27]{$27$}, \hyperref[hilb38:30]{$30$}} \\ \label{hilb38:32} $32$ & $(Q\ \vee \ P)\ \rightarrow \ (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:22]{$22$}, \hyperref[hilb38:31]{$31$}} \\ \label{hilb38:33} $33$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ D)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb38:11]{$11$} } \\ \label{hilb38:34} $34$ & $(D\ \rightarrow \ (\neg \neg P\ \vee \ Q))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ D)\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg P\ \vee \ Q$ in \hyperref[hilb38:33]{$33$} } \\ \label{hilb38:35} $35$ & $((Q\ \vee \ P)\ \rightarrow \ (\neg \neg P\ \vee \ Q))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ P))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $Q\ \vee \ P$ in \hyperref[hilb38:34]{$34$} } \\ \label{hilb38:36} $36$ & $((P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ P))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:32]{$32$}, \hyperref[hilb38:35]{$35$}} \\ \label{hilb38:37} $37$ & $(P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:23]{$23$}, \hyperref[hilb38:36]{$36$}} \\ \label{hilb38:38} $38$ & $(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.00.00.pdf}{}{hilb7}{hilb7} } \\ \label{hilb38:39} $39$ & $(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[hilb38:38]{$38$} } \\ \label{hilb38:40} $40$ & $(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[hilb38:39]{$39$} } \\ \label{hilb38:41} $41$ & $(B\ \rightarrow \ (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg P\ \vee \ Q$ in \hyperref[hilb38:40]{$40$} } \\ \label{hilb38:42} $42$ & $((P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb38:41]{$41$} } \\ \label{hilb38:43} $43$ & $\neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:37]{$37$}, \hyperref[hilb38:42]{$42$}} \\ \label{hilb38:44} $44$ & $(B\ \rightarrow \ \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg (P\ \vee \ Q)$ in \hyperref[hilb38:40]{$40$} } \\ \label{hilb38:45} $45$ & $(\neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:44]{$44$} } \\ \label{hilb38:46} $46$ & $\neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:43]{$43$}, \hyperref[hilb38:45]{$45$}} \\ \label{hilb38:47} $47$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg (P\ \vee \ Q)$ in \hyperref[hilb38:18]{$18$} } \\ \label{hilb38:48} $48$ & $(D\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:47]{$47$} } \\ \label{hilb38:49} $49$ & $(\neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg (P\ \vee \ Q)$ in \hyperref[hilb38:48]{$48$} } \\ \label{hilb38:50} $50$ & $(\neg (P\ \vee \ Q)\ \vee \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:46]{$46$}, \hyperref[hilb38:49]{$49$}} \\ \label{hilb38:51} $51$ & $(B\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg B\ \vee \ \neg \neg (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg (P\ \vee \ Q)$ in \hyperref[hilb38:7]{$7$} } \\ \label{hilb38:52} $52$ & $((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb38:51]{$51$} } \\ \label{hilb38:53} $53$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q)$ in \hyperref[hilb38:11]{$11$} } \\ \label{hilb38:54} $54$ & $(D\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:53]{$53$} } \\ \label{hilb38:55} $55$ & $((\neg (P\ \vee \ Q)\ \vee \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ Q)\ \vee \ \neg \neg (P\ \vee \ Q)$ in \hyperref[hilb38:54]{$54$} } \\ \label{hilb38:56} $56$ & $(((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:50]{$50$}, \hyperref[hilb38:55]{$55$}} \\ \label{hilb38:57} $57$ & $((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:52]{$52$}, \hyperref[hilb38:56]{$56$}} \\ \label{hilb38:58} $58$ & $(\neg B\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (B\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:13]{$13$} } \\ \label{hilb38:59} $59$ & $(\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb38:58]{$58$} } \\ \label{hilb38:60} $60$ & $(D\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $(P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:53]{$53$} } \\ \label{hilb38:61} $61$ & $((\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:60]{$60$} } \\ \label{hilb38:62} $62$ & $(((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:59]{$59$}, \hyperref[hilb38:61]{$61$}} \\ \label{hilb38:63} $63$ & $((P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:57]{$57$}, \hyperref[hilb38:62]{$62$}} \\ \label{hilb38:64} $64$ & $(P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:3]{$3$}, \hyperref[hilb38:63]{$63$}} \\ \label{hilb38:65} $65$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((\neg \neg P\ \vee \ D)\ \rightarrow \ (\neg \neg P\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg P$ in \hyperref[hilb38:18]{$18$} } \\ \label{hilb38:66} $66$ & $(D\ \rightarrow \ \neg \neg Q)\ \rightarrow \ ((\neg \neg P\ \vee \ D)\ \rightarrow \ (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg Q$ in \hyperref[hilb38:65]{$65$} } \\ \label{hilb38:67} $67$ & $(Q\ \rightarrow \ \neg \neg Q)\ \rightarrow \ ((\neg \neg P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $Q$ in \hyperref[hilb38:66]{$66$} } \\ \label{hilb38:68} $68$ & $(\neg \neg P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ \neg \neg Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:14]{$14$}, \hyperref[hilb38:67]{$67$}} \\ \label{hilb38:69} $69$ & $(B\ \rightarrow \ (\neg \neg P\ \vee \ \neg \neg Q))\ \rightarrow \ (\neg (\neg \neg P\ \vee \ \neg \neg Q)\ \rightarrow \ \neg B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg P\ \vee \ \neg \neg Q$ in \hyperref[hilb38:40]{$40$} } \\ \label{hilb38:70} $70$ & $((\neg \neg P\ \vee \ Q)\ \rightarrow \ (\neg \neg P\ \vee \ \neg \neg Q))\ \rightarrow \ (\neg (\neg \neg P\ \vee \ \neg \neg Q)\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg P\ \vee \ Q$ in \hyperref[hilb38:69]{$69$} } \\ \label{hilb38:71} $71$ & $\neg (\neg \neg P\ \vee \ \neg \neg Q)\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:68]{$68$}, \hyperref[hilb38:70]{$70$}} \\ \label{hilb38:72} $72$ & $(B\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:40]{$40$} } \\ \label{hilb38:73} $73$ & $(\neg (\neg \neg P\ \vee \ \neg \neg Q)\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg (\neg \neg P\ \vee \ \neg \neg Q)$ in \hyperref[hilb38:72]{$72$} } \\ \label{hilb38:74} $74$ & $\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:71]{$71$}, \hyperref[hilb38:73]{$73$}} \\ \label{hilb38:75} $75$ & $(D\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg (\neg \neg P\ \vee \ \neg \neg Q)$ in \hyperref[hilb38:47]{$47$} } \\ \label{hilb38:76} $76$ & $(\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))\ \rightarrow \ ((\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:75]{$75$} } \\ \label{hilb38:77} $77$ & $(\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:74]{$74$}, \hyperref[hilb38:76]{$76$}} \\ \label{hilb38:78} $78$ & $(B\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg B\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:7]{$7$} } \\ \label{hilb38:79} $79$ & $((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb38:78]{$78$} } \\ \label{hilb38:80} $80$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:11]{$11$} } \\ \label{hilb38:81} $81$ & $(D\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)$ in \hyperref[hilb38:80]{$80$} } \\ \label{hilb38:82} $82$ & $((\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb38:81]{$81$} } \\ \label{hilb38:83} $83$ & $(((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:77]{$77$}, \hyperref[hilb38:82]{$82$}} \\ \label{hilb38:84} $84$ & $((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:79]{$79$}, \hyperref[hilb38:83]{$83$}} \\ \label{hilb38:85} $85$ & $(\neg B\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))\ \rightarrow \ (B\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg (\neg \neg P\ \vee \ \neg \neg Q)$ in \hyperref[hilb38:13]{$13$} } \\ \label{hilb38:86} $86$ & $(\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb38:85]{$85$} } \\ \label{hilb38:87} $87$ & $(D\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $(P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)$ in \hyperref[hilb38:80]{$80$} } \\ \label{hilb38:88} $88$ & $((\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)$ in \hyperref[hilb38:87]{$87$} } \\ \label{hilb38:89} $89$ & $(((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \vee \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:86]{$86$}, \hyperref[hilb38:88]{$88$}} \\ \label{hilb38:90} $90$ & $((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:84]{$84$}, \hyperref[hilb38:89]{$89$}} \\ \label{hilb38:91} $91$ & $(P\ \vee \ Q)\ \rightarrow \ \neg \neg (\neg \neg P\ \vee \ \neg \neg Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb38:64]{$64$}, \hyperref[hilb38:90]{$90$}} \\ \label{hilb38:92} $92$ & $(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:91]{$91$} 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$ & $\neg \neg P\ \rightarrow \ P$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{hilb6}{hilb6} } \\ \label{hilb39:2} $2$ & $\neg \neg A\ \rightarrow \ A$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $A$ in \hyperref[hilb39:1]{$1$} } \\ \label{hilb39:3} $3$ & $\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P\ \vee \ Q$ in \hyperref[hilb39:2]{$2$} } \\ \label{hilb39:4} $4$ & $(P\ \rightarrow \ Q)\ \rightarrow \ (\neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl1}{defimpl1} } \\ \label{hilb39:5} $5$ & $(\neg P\ \vee \ Q)\ \rightarrow \ (P\ \rightarrow \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule3}{add sentence} \hyperref{prophilbert1_1.00.00_1.00.00.pdf}{}{defimpl2}{defimpl2} } \\ \label{hilb39:6} $6$ & $(P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule2}{add axiom} \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{axiom3}{axiom3} } \\ \label{hilb39:7} $7$ & $(P\ \vee \ A)\ \rightarrow \ (A\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $A$ in \hyperref[hilb39:6]{$6$} } \\ \label{hilb39:8} $8$ & $(B\ \vee \ A)\ \rightarrow \ (A\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[hilb39:7]{$7$} } \\ \label{hilb39:9} $9$ & $(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.00.00.pdf}{}{hilb1}{hilb1} } \\ \label{hilb39:10} $10$ & $(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[hilb39:9]{$9$} } \\ \label{hilb39:11} $11$ & $(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[hilb39:10]{$10$} } \\ \label{hilb39:12} $12$ & $(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[hilb39:11]{$11$} } \\ \label{hilb39:13} $13$ & $(B\ \vee \ (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P\ \vee \ Q$ in \hyperref[hilb39:8]{$8$} } \\ \label{hilb39:14} $14$ & $(P\ \rightarrow \ A)\ \rightarrow \ (\neg P\ \vee \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $A$ in \hyperref[hilb39:4]{$4$} } \\ \label{hilb39:15} $15$ & $(B\ \rightarrow \ A)\ \rightarrow \ (\neg B\ \vee \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[hilb39:14]{$14$} } \\ \label{hilb39:16} $16$ & $(B\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg B\ \vee \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P\ \vee \ Q$ in \hyperref[hilb39:15]{$15$} } \\ \label{hilb39:17} $17$ & $(\neg P\ \vee \ A)\ \rightarrow \ (P\ \rightarrow \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $Q$ by $A$ in \hyperref[hilb39:5]{$5$} } \\ \label{hilb39:18} $18$ & $(\neg B\ \vee \ A)\ \rightarrow \ (B\ \rightarrow \ A)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $P$ by $B$ in \hyperref[hilb39:17]{$17$} } \\ \label{hilb39:19} $19$ & $(\neg B\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (B\ \rightarrow \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P\ \vee \ Q$ in \hyperref[hilb39:18]{$18$} } \\ \label{hilb39:20} $20$ & $\neg \neg 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:21} $21$ & $(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{hilb39:22} $22$ & $(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[hilb39:21]{$21$} } \\ \label{hilb39:23} $23$ & $(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[hilb39:22]{$22$} } \\ \label{hilb39:24} $24$ & $(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[hilb39:23]{$23$} } \\ \label{hilb39:25} $25$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((Q\ \vee \ D)\ \rightarrow \ (Q\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q$ in \hyperref[hilb39:24]{$24$} } \\ \label{hilb39:26} $26$ & $(D\ \rightarrow \ P)\ \rightarrow \ ((Q\ \vee \ D)\ \rightarrow \ (Q\ \vee \ P))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $P$ in \hyperref[hilb39:25]{$25$} } \\ \label{hilb39:27} $27$ & $(\neg \neg P\ \rightarrow \ P)\ \rightarrow \ ((Q\ \vee \ \neg \neg P)\ \rightarrow \ (Q\ \vee \ P))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg P$ in \hyperref[hilb39:26]{$26$} } \\ \label{hilb39:28} $28$ & $(Q\ \vee \ \neg \neg P)\ \rightarrow \ (Q\ \vee \ P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:1]{$1$}, \hyperref[hilb39:27]{$27$}} \\ \label{hilb39:29} $29$ & $(B\ \vee \ P)\ \rightarrow \ (P\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P$ in \hyperref[hilb39:8]{$8$} } \\ \label{hilb39:30} $30$ & $(Q\ \vee \ P)\ \rightarrow \ (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q$ in \hyperref[hilb39:29]{$29$} } \\ \label{hilb39:31} $31$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((Q\ \vee \ \neg \neg P)\ \rightarrow \ D)\ \rightarrow \ ((Q\ \vee \ \neg \neg P)\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $Q\ \vee \ \neg \neg P$ in \hyperref[hilb39:12]{$12$} } \\ \label{hilb39:32} $32$ & $(D\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (((Q\ \vee \ \neg \neg P)\ \rightarrow \ D)\ \rightarrow \ ((Q\ \vee \ \neg \neg P)\ \rightarrow \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $P\ \vee \ Q$ in \hyperref[hilb39:31]{$31$} } \\ \label{hilb39:33} $33$ & $((Q\ \vee \ P)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (((Q\ \vee \ \neg \neg P)\ \rightarrow \ (Q\ \vee \ P))\ \rightarrow \ ((Q\ \vee \ \neg \neg P)\ \rightarrow \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $Q\ \vee \ P$ in \hyperref[hilb39:32]{$32$} } \\ \label{hilb39:34} $34$ & $((Q\ \vee \ \neg \neg P)\ \rightarrow \ (Q\ \vee \ P))\ \rightarrow \ ((Q\ \vee \ \neg \neg P)\ \rightarrow \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:30]{$30$}, \hyperref[hilb39:33]{$33$}} \\ \label{hilb39:35} $35$ & $(Q\ \vee \ \neg \neg P)\ \rightarrow \ (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:28]{$28$}, \hyperref[hilb39:34]{$34$}} \\ \label{hilb39:36} $36$ & $(B\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $Q$ in \hyperref[hilb39:8]{$8$} } \\ \label{hilb39:37} $37$ & $(\neg \neg P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ \neg \neg P)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg P$ in \hyperref[hilb39:36]{$36$} } \\ \label{hilb39:38} $38$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((\neg \neg P\ \vee \ Q)\ \rightarrow \ D)\ \rightarrow \ ((\neg \neg P\ \vee \ Q)\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg P\ \vee \ Q$ in \hyperref[hilb39:12]{$12$} } \\ \label{hilb39:39} $39$ & $(D\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (((\neg \neg P\ \vee \ Q)\ \rightarrow \ D)\ \rightarrow \ ((\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $P\ \vee \ Q$ in \hyperref[hilb39:38]{$38$} } \\ \label{hilb39:40} $40$ & $((Q\ \vee \ \neg \neg P)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (((\neg \neg P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ \neg \neg P))\ \rightarrow \ ((\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $Q\ \vee \ \neg \neg P$ in \hyperref[hilb39:39]{$39$} } \\ \label{hilb39:41} $41$ & $((\neg \neg P\ \vee \ Q)\ \rightarrow \ (Q\ \vee \ \neg \neg P))\ \rightarrow \ ((\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:35]{$35$}, \hyperref[hilb39:40]{$40$}} \\ \label{hilb39:42} $42$ & $(\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:37]{$37$}, \hyperref[hilb39:41]{$41$}} \\ \label{hilb39:43} $43$ & $(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.00.00.pdf}{}{hilb7}{hilb7} } \\ \label{hilb39:44} $44$ & $(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[hilb39:43]{$43$} } \\ \label{hilb39:45} $45$ & $(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[hilb39:44]{$44$} } \\ \label{hilb39:46} $46$ & $(B\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \rightarrow \ \neg B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $P\ \vee \ Q$ in \hyperref[hilb39:45]{$45$} } \\ \label{hilb39:47} $47$ & $((\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg (P\ \vee \ Q)\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg P\ \vee \ Q$ in \hyperref[hilb39:46]{$46$} } \\ \label{hilb39:48} $48$ & $\neg (P\ \vee \ Q)\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:42]{$42$}, \hyperref[hilb39:47]{$47$}} \\ \label{hilb39:49} $49$ & $(B\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb39:45]{$45$} } \\ \label{hilb39:50} $50$ & $(\neg (P\ \vee \ Q)\ \rightarrow \ \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg (P\ \vee \ Q)$ in \hyperref[hilb39:49]{$49$} } \\ \label{hilb39:51} $51$ & $\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:48]{$48$}, \hyperref[hilb39:50]{$50$}} \\ \label{hilb39:52} $52$ & $(B\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg (P\ \vee \ Q)$ in \hyperref[hilb39:45]{$45$} } \\ \label{hilb39:53} $53$ & $(\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb39:52]{$52$} } \\ \label{hilb39:54} $54$ & $\neg \neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg \neg \neg (\neg \neg P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:51]{$51$}, \hyperref[hilb39:53]{$53$}} \\ \label{hilb39:55} $55$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb39:24]{$24$} } \\ \label{hilb39:56} $56$ & $(D\ \rightarrow \ \neg \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (((P\ \vee \ Q)\ \vee \ D)\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb39:55]{$55$} } \\ \label{hilb39:57} $57$ & $(\neg \neg \neg (P\ \vee \ Q)\ \rightarrow \ \neg \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg \neg (P\ \vee \ Q)$ in \hyperref[hilb39:56]{$56$} } \\ \label{hilb39:58} $58$ & $((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:54]{$54$}, \hyperref[hilb39:57]{$57$}} \\ \label{hilb39:59} $59$ & $(B\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ B)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $A$ by $\neg \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb39:8]{$8$} } \\ \label{hilb39:60} $60$ & $((P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $P\ \vee \ Q$ in \hyperref[hilb39:59]{$59$} } \\ \label{hilb39:61} $61$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $(P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q)$ in \hyperref[hilb39:12]{$12$} } \\ \label{hilb39:62} $62$ & $(D\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ (((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)$ in \hyperref[hilb39:61]{$61$} } \\ \label{hilb39:63} $63$ & $(((P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ ((((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb39:62]{$62$} } \\ \label{hilb39:64} $64$ & $(((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (\neg \neg P\ \vee \ Q)))\ \rightarrow \ (((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:60]{$60$}, \hyperref[hilb39:63]{$63$}} \\ \label{hilb39:65} $65$ & $((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:58]{$58$}, \hyperref[hilb39:64]{$64$}} \\ \label{hilb39:66} $66$ & $(\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \neg (P\ \vee \ Q)$ in \hyperref[hilb39:13]{$13$} } \\ \label{hilb39:67} $67$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ ((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)$ in \hyperref[hilb39:12]{$12$} } \\ \label{hilb39:68} $68$ & $(D\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ (((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ ((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)$ in \hyperref[hilb39:67]{$67$} } \\ \label{hilb39:69} $69$ & $(((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ (((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q)))\ \rightarrow \ ((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $(P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q)$ in \hyperref[hilb39:68]{$68$} } \\ \label{hilb39:70} $70$ & $((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ ((P\ \vee \ Q)\ \vee \ \neg \neg \neg (P\ \vee \ Q)))\ \rightarrow \ ((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:65]{$65$}, \hyperref[hilb39:69]{$69$}} \\ \label{hilb39:71} $71$ & $(\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:66]{$66$}, \hyperref[hilb39:70]{$70$}} \\ \label{hilb39:72} $72$ & $(\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg (P\ \vee \ Q)$ in \hyperref[hilb39:16]{$16$} } \\ \label{hilb39:73} $73$ & $(D\ \rightarrow \ C)\ \rightarrow \ (((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ ((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)$ in \hyperref[hilb39:12]{$12$} } \\ \label{hilb39:74} $74$ & $(D\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ (((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ ((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)$ in \hyperref[hilb39:73]{$73$} } \\ \label{hilb39:75} $75$ & $((\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ (((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ ((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)$ in \hyperref[hilb39:74]{$74$} } \\ \label{hilb39:76} $76$ & $((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ ((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:71]{$71$}, \hyperref[hilb39:75]{$75$}} \\ \label{hilb39:77} $77$ & $(\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:72]{$72$}, \hyperref[hilb39:76]{$76$}} \\ \label{hilb39:78} $78$ & $(\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg (\neg \neg P\ \vee \ Q)$ in \hyperref[hilb39:19]{$19$} } \\ \label{hilb39:79} $79$ & $(D\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)))\ \rightarrow \ (((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ D)\ \rightarrow \ ((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)$ in \hyperref[hilb39:73]{$73$} } \\ \label{hilb39:80} $80$ & $((\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)))\ \rightarrow \ (((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ ((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)$ in \hyperref[hilb39:79]{$79$} } \\ \label{hilb39:81} $81$ & $((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg \neg (\neg \neg P\ \vee \ Q)\ \vee \ (P\ \vee \ Q)))\ \rightarrow \ ((\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:78]{$78$}, \hyperref[hilb39:80]{$80$}} \\ \label{hilb39:82} $82$ & $(\neg \neg (P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))\ \rightarrow \ (\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:77]{$77$}, \hyperref[hilb39:81]{$81$}} \\ \label{hilb39:83} $83$ & $\neg \neg (\neg \neg P\ \vee \ Q)\ \rightarrow \ (P\ \vee \ Q)$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule1}{MP} with \hyperref[hilb39:3]{$3$}, \hyperref[hilb39:82]{$82$}} \\ \label{hilb39:84} $84$ & $(D\ \rightarrow \ C)\ \rightarrow \ ((\neg \neg P\ \vee \ D)\ \rightarrow \ (\neg \neg P\ \vee \ C))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $B$ by $\neg \neg P$ in \hyperref[hilb39:24]{$24$} } \\ \label{hilb39:85} $85$ & $(D\ \rightarrow \ Q)\ \rightarrow \ ((\neg \neg P\ \vee \ D)\ \rightarrow \ (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $C$ by $Q$ in \hyperref[hilb39:84]{$84$} } \\ \label{hilb39:86} $86$ & $(\neg \neg Q\ \rightarrow \ Q)\ \rightarrow \ ((\neg \neg P\ \vee \ \neg \neg Q)\ \rightarrow \ (\neg \neg P\ \vee \ Q))$ & {\tiny \hyperref{propaxiom_1.00.00_1.00.00.pdf}{}{rule4}{replace} $D$ by $\neg \neg Q$ in \hyperref[hilb39:85]{$85$} } \\ \label{