Nuprl Lemma : DeMorgan3
[P,Q:
]. (((
P) 
(Q)) 
((P 
Q)))
Proof
Definitions occuring in Statement :
uall: [x:A]. B[x],
prop: ,
not: A,
implies: P Q,
or: P Q,
and: P Q
Definitions :
implies: P Q,
not: A,
member: t 
T,
prop: ,
and: P Q,
uall: [x:A]. B[x],
or: P Q
Lemmas :
or_wf,
not_wf
\mforall{}[P,Q:\mBbbP{}]. (((\mneg{}P) \mwedge{} (\mneg{}Q)) {}\mRightarrow{} (\mneg{}(P \mvee{} Q)))
Date html generated:
2013_09_05-AM-11_13_27
Last ObjectModification:
2013_07_09-PM-01_56_32
Home
Index