Nuprl Lemma : implication1
[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,
or: P Q,
not: A,
false: False
Lemmas :
or_wf,
not_wf
\mforall{}[P,Q:\mBbbP{}]. (((\mneg{}P) \mvee{} Q) {}\mRightarrow{} P {}\mRightarrow{} Q)
Date html generated:
2013_09_05-AM-11_13_39
Last ObjectModification:
2013_07_09-PM-02_54_43
Home
Index