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