\indexentry{\alpha * macro modus ponens * @\back \makebox[20mm][l]{$[ \mathsf{x} \unrhd \mathsf{y}]$}* macro modus ponens *|hyperpage}{8}
\indexentry{pyk: * macro modus ponens * $[ \mathsf{x} \unrhd \mathsf{y}]$|hyperpage}{8}
\indexentry{\alpha double rule prime mp @\back \makebox[20mm][l]{$[MP'_{d}]$}double rule prime mp|hyperpage}{8}
\indexentry{pyk: double rule prime mp $[MP'_{d}]$|hyperpage}{8}
\indexentry{\alpha * macro first modus ponens * macro second modus ponens * @\back \makebox[20mm][l]{$[ \mathsf{x} \unrhd \mathsf{y} \unrhd \mathsf{z}]$}* macro first modus ponens * macro second modus ponens *|hyperpage}{8}
\indexentry{pyk: * macro first modus ponens * macro second modus ponens * $[ \mathsf{x} \unrhd \mathsf{y} \unrhd \mathsf{z}]$|hyperpage}{8}
\indexentry{\alpha inference axiom prime a one @\back \makebox[20mm][l]{$[A1'_{i}]$}inference axiom prime a one|hyperpage}{9}
\indexentry{pyk: inference axiom prime a one $[A1'_{i}]$|hyperpage}{9}
\indexentry{\alpha rule hypothesize @\back \makebox[20mm][l]{$[Hypothesize]$}rule hypothesize|hyperpage}{9}
\indexentry{pyk: rule hypothesize $[Hypothesize]$|hyperpage}{9}
\indexentry{\alpha inference axiom prime a two @\back \makebox[20mm][l]{$[A2'_{i}]$}inference axiom prime a two|hyperpage}{9}
\indexentry{pyk: inference axiom prime a two $[A2'_{i}]$|hyperpage}{9}
\indexentry{\alpha inference inference axiom prime a two @\back \makebox[20mm][l]{$[A2'_{ii}]$}inference inference axiom prime a two|hyperpage}{9}
\indexentry{pyk: inference inference axiom prime a two $[A2'_{ii}]$|hyperpage}{9}
\indexentry{\alpha hypothetical rule prime mp @\back \makebox[20mm][l]{$[MP'_{h}]$}hypothetical rule prime mp|hyperpage}{10}
\indexentry{pyk: hypothetical rule prime mp $[MP'_{h}]$|hyperpage}{10}
\indexentry{\alpha * hypothetical macro modus ponens * @\back \makebox[20mm][l]{$[ \mathsf{x} \unrhd_h \mathsf{y}]$}* hypothetical macro modus ponens *|hyperpage}{10}
\indexentry{pyk: * hypothetical macro modus ponens * $[ \mathsf{x} \unrhd_h \mathsf{y}]$|hyperpage}{10}
\indexentry{\alpha double inference inference axiom prime a two @\back \makebox[20mm][l]{$[A2'_{iid}]$}double inference inference axiom prime a two|hyperpage}{10}
\indexentry{pyk: double inference inference axiom prime a two $[A2'_{iid}]$|hyperpage}{10}
\indexentry{\alpha double hypothetical rule prime mp @\back \makebox[20mm][l]{$[MP'_{hd}]$}double hypothetical rule prime mp|hyperpage}{10}
\indexentry{pyk: double hypothetical rule prime mp $[MP'_{hd}]$|hyperpage}{10}
\indexentry{\alpha * hypothetical macro first modus ponens * hypothetical macro second modus ponens var * @\back \makebox[20mm][l]{$[ \mathsf{x} \unrhd_h \mathsf{y} \unrhd_h \mathsf{z}]$}* hypothetical macro first modus ponens * hypothetical macro second modus ponens var *|hyperpage}{10}
\indexentry{pyk: * hypothetical macro first modus ponens * hypothetical macro second modus ponens var * $[ \mathsf{x} \unrhd_h \mathsf{y} \unrhd_h \mathsf{z}]$|hyperpage}{10}
\indexentry{\alpha mendelson lemma one eight @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.8}]$}mendelson lemma one eight|hyperpage}{11}
\indexentry{pyk: mendelson lemma one eight $[Mendelson\ \textbf{1.8}]$|hyperpage}{11}
\indexentry{\alpha inference mendelson lemma one eight @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.8}_{i}]$}inference mendelson lemma one eight|hyperpage}{11}
\indexentry{pyk: inference mendelson lemma one eight $[Mendelson\ \textbf{1.8}_{i}]$|hyperpage}{11}
\indexentry{\alpha rule repetition @\back \makebox[20mm][l]{$[Repetition]$}rule repetition|hyperpage}{11}
\indexentry{pyk: rule repetition $[Repetition]$|hyperpage}{11}
\indexentry{\alpha mendelson exercise one fourtyseven b @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.47}\ b]$}mendelson exercise one fourtyseven b|hyperpage}{11}
\indexentry{pyk: mendelson exercise one fourtyseven b $[Mendelson\ \textbf{1.47}\ b]$|hyperpage}{11}
\indexentry{\alpha mendelson exercise one fourtyseven c @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.47}\ c]$}mendelson exercise one fourtyseven c|hyperpage}{12}
\indexentry{pyk: mendelson exercise one fourtyseven c $[Mendelson\ \textbf{1.47}\ c]$|hyperpage}{12}
\indexentry{\alpha mendelson exercise one fourtyseven e @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.47}\ e]$}mendelson exercise one fourtyseven e|hyperpage}{12}
\indexentry{pyk: mendelson exercise one fourtyseven e $[Mendelson\ \textbf{1.47}\ e]$|hyperpage}{12}
\indexentry{\alpha hypothesis @\back \makebox[20mm][l]{$[\mathsf{hyp}]$}hypothesis|hyperpage}{13}
\indexentry{pyk: hypothesis $[\mathsf{hyp}]$|hyperpage}{13}
\indexentry{\alpha instance @\back \makebox[20mm][l]{$[\mathsf{instance}]$}instance|hyperpage}{13}
\indexentry{pyk: instance $[\mathsf{instance}]$|hyperpage}{13}
\indexentry{\alpha conclusion @\back \makebox[20mm][l]{$[\mathsf{conclusion}]$}conclusion|hyperpage}{13}
\indexentry{pyk: conclusion $[\mathsf{conclusion}]$|hyperpage}{13}
\indexentry{\alpha mendelson lemma one eleven d @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.11}\ d]$}mendelson lemma one eleven d|hyperpage}{15}
\indexentry{pyk: mendelson lemma one eleven d $[Mendelson\ \textbf{1.11}\ d]$|hyperpage}{15}
\indexentry{\alpha line * hypothesis indeed * end line * @\back \makebox[20mm][l]{$[ Line \, \mathsf {l} :\bullet{}\ Hypothesis \gg \mathsf {i} ; \mathsf {p}]$}line * hypothesis indeed * end line *|hyperpage}{16}
\indexentry{pyk: line * hypothesis indeed * end line * $[ Line \, \mathsf {l} :\bullet{}\ Hypothesis \gg \mathsf {i} ; \mathsf {p}]$|hyperpage}{16}
\indexentry{\alpha line * hypothesis because * indeed * end line * @\back \makebox[20mm][l]{$[ Line \, \mathsf {l} :\bullet{}\ \mathsf {a} \gg \mathsf {i} ; \mathsf {p}]$}line * hypothesis because * indeed * end line *|hyperpage}{17}
\indexentry{pyk: line * hypothesis because * indeed * end line * $[ Line \, \mathsf {l} :\bullet{}\ \mathsf {a} \gg \mathsf {i} ; \mathsf {p}]$|hyperpage}{17}
\indexentry{\alpha line * hypothesis raw because * indeed * end line * @\back \makebox[20mm][l]{$[ Line \, \mathsf {l} :\bullet{}\ \mathsf {a} \gg \mathsf {i} ; \mathsf {p}]$}line * hypothesis raw because * indeed * end line *|hyperpage}{17}
\indexentry{pyk: line * hypothesis raw because * indeed * end line * $[ Line \, \mathsf {l} :\bullet{}\ \mathsf {a} \gg \mathsf {i} ; \mathsf {p}]$|hyperpage}{17}
\indexentry{\alpha line * hypothesis modus ponens * modus ponens * indeed * end line * @\back \makebox[20mm][l]{$[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \unrhd{} \mathsf {v} \gg \mathsf {i} ; \mathsf {p}]$}line * hypothesis modus ponens * modus ponens * indeed * end line *|hyperpage}{18}
\indexentry{pyk: line * hypothesis modus ponens * modus ponens * indeed * end line * $[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \unrhd{} \mathsf {v} \gg \mathsf {i} ; \mathsf {p}]$|hyperpage}{18}
\indexentry{\alpha line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line * @\back \makebox[20mm][l]{$[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \unrhd{} \mathsf {v} \unrhd{} \mathsf{z} \gg \mathsf {i} ; \mathsf {p}]$}line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line *|hyperpage}{18}
\indexentry{pyk: line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line * $[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \unrhd{} \mathsf {v} \unrhd{} \mathsf{z} \gg \mathsf {i} ; \mathsf {p}]$|hyperpage}{18}
\indexentry{\alpha line * hypothesis first modus ponens * modus ponens * indeed * end line * @\back \makebox[20mm][l]{$[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \circ{} \unrhd{} \mathsf {v} \gg \mathsf {i} ; \mathsf {p}]$}line * hypothesis first modus ponens * modus ponens * indeed * end line *|hyperpage}{18}
\indexentry{pyk: line * hypothesis first modus ponens * modus ponens * indeed * end line * $[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \circ{} \unrhd{} \mathsf {v} \gg \mathsf {i} ; \mathsf {p}]$|hyperpage}{18}
\indexentry{\alpha line * hypothesis second modus ponens * modus ponens * indeed * end line * @\back \makebox[20mm][l]{$[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \unrhd{} \mathsf {v} \circ{} \gg \mathsf {i} ; \mathsf {p}]$}line * hypothesis second modus ponens * modus ponens * indeed * end line *|hyperpage}{18}
\indexentry{pyk: line * hypothesis second modus ponens * modus ponens * indeed * end line * $[ Line \, \mathsf {l} :\bullet{}\ \mathsf {u} \unrhd{} \mathsf {v} \circ{} \gg \mathsf {i} ; \mathsf {p}]$|hyperpage}{18}
\indexentry{\alpha hypothetical inference axiom prime a one @\back \makebox[20mm][l]{$[A1'_{ih}]$}hypothetical inference axiom prime a one|hyperpage}{19}
\indexentry{pyk: hypothetical inference axiom prime a one $[A1'_{ih}]$|hyperpage}{19}
\indexentry{\alpha hypothetical inference axiom prime a two @\back \makebox[20mm][l]{$[A2'_{ih}]$}hypothetical inference axiom prime a two|hyperpage}{19}
\indexentry{pyk: hypothetical inference axiom prime a two $[A2'_{ih}]$|hyperpage}{19}
\indexentry{\alpha hypothetical inference inference axiom prime a two @\back \makebox[20mm][l]{$[A2'_{iih}]$}hypothetical inference inference axiom prime a two|hyperpage}{20}
\indexentry{pyk: hypothetical inference inference axiom prime a two $[A2'_{iih}]$|hyperpage}{20}
\indexentry{\alpha hypothetical mendelson exercise one fourtyseven b @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.47}\ b_{h}]$}hypothetical mendelson exercise one fourtyseven b|hyperpage}{20}
\indexentry{pyk: hypothetical mendelson exercise one fourtyseven b $[Mendelson\ \textbf{1.47}\ b_{h}]$|hyperpage}{20}
\indexentry{\alpha hypothetical mendelson exercise one fourtyseven c @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.47}\ c_{h}]$}hypothetical mendelson exercise one fourtyseven c|hyperpage}{21}
\indexentry{pyk: hypothetical mendelson exercise one fourtyseven c $[Mendelson\ \textbf{1.47}\ c_{h}]$|hyperpage}{21}
\indexentry{\alpha mendelson lemma one eleven c @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.11}\ c]$}mendelson lemma one eleven c|hyperpage}{21}
\indexentry{pyk: mendelson lemma one eleven c $[Mendelson\ \textbf{1.11}\ c]$|hyperpage}{21}
\indexentry{\alpha mendelson exercise one fourtyeight d @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.48}\ d]$}mendelson exercise one fourtyeight d|hyperpage}{22}
\indexentry{pyk: mendelson exercise one fourtyeight d $[Mendelson\ \textbf{1.48}\ d]$|hyperpage}{22}
\indexentry{\alpha mendelson exercise one fourtyeight e @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.48}\ e]$}mendelson exercise one fourtyeight e|hyperpage}{22}
\indexentry{pyk: mendelson exercise one fourtyeight e $[Mendelson\ \textbf{1.48}\ e]$|hyperpage}{22}
\indexentry{\alpha mendelson exercise one fourtyeight h @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.48}\ h]$}mendelson exercise one fourtyeight h|hyperpage}{22}
\indexentry{pyk: mendelson exercise one fourtyeight h $[Mendelson\ \textbf{1.48}\ h]$|hyperpage}{22}
\indexentry{\alpha mendelson corollary one ten a @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.10}\ a]$}mendelson corollary one ten a|hyperpage}{23}
\indexentry{pyk: mendelson corollary one ten a $[Mendelson\ \textbf{1.10}\ a]$|hyperpage}{23}
\indexentry{\alpha mendelson corollary one ten b @\back \makebox[20mm][l]{$[Mendelson\ \textbf{1.10}\ b]$}mendelson corollary one ten b|hyperpage}{23}
\indexentry{pyk: mendelson corollary one ten b $[Mendelson\ \textbf{1.10}\ b]$|hyperpage}{23}
\indexentry{\alpha inference axiom prime s one @\back \makebox[20mm][l]{$[S1'_{i}]$}inference axiom prime s one|hyperpage}{25}
\indexentry{pyk: inference axiom prime s one $[S1'_{i}]$|hyperpage}{25}
\indexentry{\alpha inference inference axiom prime s one @\back \makebox[20mm][l]{$[S1'_{ii}]$}inference inference axiom prime s one|hyperpage}{25}
\indexentry{pyk: inference inference axiom prime s one $[S1'_{ii}]$|hyperpage}{25}
\indexentry{\alpha inference axiom prime s two @\back \makebox[20mm][l]{$[S2'_{i}]$}inference axiom prime s two|hyperpage}{26}
\indexentry{pyk: inference axiom prime s two $[S2'_{i}]$|hyperpage}{26}
\indexentry{\alpha hypothetical inference axiom prime s two @\back \makebox[20mm][l]{$[S2'_{ih}]$}hypothetical inference axiom prime s two|hyperpage}{26}
\indexentry{pyk: hypothetical inference axiom prime s two $[S2'_{ih}]$|hyperpage}{26}
\indexentry{\alpha inference inference axiom prime s nine @\back \makebox[20mm][l]{$[S9'_{ii}]$}inference inference axiom prime s nine|hyperpage}{26}
\indexentry{pyk: inference inference axiom prime s nine $[S9'_{ii}]$|hyperpage}{26}
\indexentry{\alpha rule induction @\back \makebox[20mm][l]{$[Induction]$}rule induction|hyperpage}{27}
\indexentry{pyk: rule induction $[Induction]$|hyperpage}{27}
\indexentry{\alpha mendelson proposition three two a @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ a]$}mendelson proposition three two a|hyperpage}{28}
\indexentry{pyk: mendelson proposition three two a $[Mendelson\ \textbf{3.2}\ a]$|hyperpage}{28}
\indexentry{\alpha mendelson proposition three two b @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ b]$}mendelson proposition three two b|hyperpage}{28}
\indexentry{pyk: mendelson proposition three two b $[Mendelson\ \textbf{3.2}\ b]$|hyperpage}{28}
\indexentry{\alpha inference mendelson proposition three two b @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ b_{i}]$}inference mendelson proposition three two b|hyperpage}{28}
\indexentry{pyk: inference mendelson proposition three two b $[Mendelson\ \textbf{3.2}\ b_{i}]$|hyperpage}{28}
\indexentry{\alpha mendelson proposition three two c @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ c]$}mendelson proposition three two c|hyperpage}{29}
\indexentry{pyk: mendelson proposition three two c $[Mendelson\ \textbf{3.2}\ c]$|hyperpage}{29}
\indexentry{\alpha inference inference mendelson proposition three two c @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ c_{ii}]$}inference inference mendelson proposition three two c|hyperpage}{29}
\indexentry{pyk: inference inference mendelson proposition three two c $[Mendelson\ \textbf{3.2}\ c_{ii}]$|hyperpage}{29}
\indexentry{\alpha hypothetical inference inference mendelson proposition three two c @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ c_{iih}]$}hypothetical inference inference mendelson proposition three two c|hyperpage}{29}
\indexentry{pyk: hypothetical inference inference mendelson proposition three two c $[Mendelson\ \textbf{3.2}\ c_{iih}]$|hyperpage}{29}
\indexentry{\alpha mendelson proposition three two d @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ d]$}mendelson proposition three two d|hyperpage}{30}
\indexentry{pyk: mendelson proposition three two d $[Mendelson\ \textbf{3.2}\ d]$|hyperpage}{30}
\indexentry{\alpha inference inference mendelson proposition three two d @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ d_{ii}]$}inference inference mendelson proposition three two d|hyperpage}{30}
\indexentry{pyk: inference inference mendelson proposition three two d $[Mendelson\ \textbf{3.2}\ d_{ii}]$|hyperpage}{30}
\indexentry{\alpha hypothetical inference inference mendelson proposition three two d @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ d_{iih}]$}hypothetical inference inference mendelson proposition three two d|hyperpage}{31}
\indexentry{pyk: hypothetical inference inference mendelson proposition three two d $[Mendelson\ \textbf{3.2}\ d_{iih}]$|hyperpage}{31}
\indexentry{\alpha mendelson proposition three two f i @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ f\ i]$}mendelson proposition three two f i|hyperpage}{31}
\indexentry{pyk: mendelson proposition three two f i $[Mendelson\ \textbf{3.2}\ f\ i]$|hyperpage}{31}
\indexentry{\alpha mendelson proposition three two f ii @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ f\ ii]$}mendelson proposition three two f ii|hyperpage}{31}
\indexentry{pyk: mendelson proposition three two f ii $[Mendelson\ \textbf{3.2}\ f\ ii]$|hyperpage}{31}
\indexentry{\alpha mendelson proposition three two f @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ f]$}mendelson proposition three two f|hyperpage}{31}
\indexentry{pyk: mendelson proposition three two f $[Mendelson\ \textbf{3.2}\ f]$|hyperpage}{31}
\indexentry{\alpha mendelson proposition three two g i @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ g\ i]$}mendelson proposition three two g i|hyperpage}{32}
\indexentry{pyk: mendelson proposition three two g i $[Mendelson\ \textbf{3.2}\ g\ i]$|hyperpage}{32}
\indexentry{\alpha mendelson proposition three two g ii @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ g\ ii]$}mendelson proposition three two g ii|hyperpage}{32}
\indexentry{pyk: mendelson proposition three two g ii $[Mendelson\ \textbf{3.2}\ g\ ii]$|hyperpage}{32}
\indexentry{\alpha mendelson proposition three two g @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ g]$}mendelson proposition three two g|hyperpage}{32}
\indexentry{pyk: mendelson proposition three two g $[Mendelson\ \textbf{3.2}\ g]$|hyperpage}{32}
\indexentry{\alpha mendelson proposition three two h i @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ h\ i]$}mendelson proposition three two h i|hyperpage}{33}
\indexentry{pyk: mendelson proposition three two h i $[Mendelson\ \textbf{3.2}\ h\ i]$|hyperpage}{33}
\indexentry{\alpha mendelson proposition three two h ii @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ h\ ii]$}mendelson proposition three two h ii|hyperpage}{33}
\indexentry{pyk: mendelson proposition three two h ii $[Mendelson\ \textbf{3.2}\ h\ ii]$|hyperpage}{33}
\indexentry{\alpha mendelson proposition three two h @\back \makebox[20mm][l]{$[Mendelson\ \textbf{3.2}\ h]$}mendelson proposition three two h|hyperpage}{33}
\indexentry{pyk: mendelson proposition three two h $[Mendelson\ \textbf{3.2}\ h]$|hyperpage}{33}