Nuprl Lemma : implication2
[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
Definitions :
uall: [x:A]. B[x],
member: t 
T,
prop: ,
implies: P Q,
not: A,
or: P Q,
guard: {T}
Lemmas :
not_wf,
or_wf,
false_wf
\mforall{}[P,Q:\mBbbP{}]. ((P {}\mRightarrow{} Q) {}\mRightarrow{} (\mneg{}\mneg{}((\mneg{}P) \mvee{} Q)))
Date html generated:
2013_09_05-AM-11_13_44
Last ObjectModification:
2013_07_09-PM-03_53_32
Home
Index