Nuprl Lemma : DeMorgan1
[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) \mvee{} (\mneg{}Q)) {}\mRightarrow{} (\mneg{}(P \mwedge{} Q)))
Date html generated:
2013_09_05-AM-11_13_15
Last ObjectModification:
2013_07_08-PM-04_57_25
Home
Index