Step
*
of Lemma
notnot_P_or_notP
[P:
].
(
(P
(
P)))
BY
{
(UD
THENA
Auto)
}
1
1.
[P]
:
(P
(
P))
Latex:
\mforall{}[P:\mBbbP{}]. (\mneg{}\mneg{}(P \mvee{} (\mneg{}P)))
By
(UD THENA Auto)
Home
Index
[P:
]. (
(P 
(P)))
(P (P))