Nuprl Lemma : logic7
[P,Q:
].  ((P 
 (
P)) 
 P 
 Q)
Proof
Definitions occuring in Statement : 
uall:
[x:A]. B[x], 
prop:
, 
not:
A, 
implies: P 
 Q
Definitions : 
uall:
[x:A]. B[x], 
member: t 
 T, 
prop:
, 
implies: P 
 Q, 
not:
A, 
false: False
Lemmas : 
not_wf
\mforall{}[P,Q:\mBbbP{}].    ((P  {}\mRightarrow{}  (\mneg{}P))  {}\mRightarrow{}  P  {}\mRightarrow{}  Q)
Date html generated:
2013_09_05-AM-11_12_50
Last ObjectModification:
2013_06_03-PM-01_21_11
Home
Index