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