Nuprl Lemma : logic4

[P,Q:

]. ((

P)

P

Q)

Proof

Definitions occuring in Statement : uall:

[x:A]. B[x], prop:

, not:

A, implies: P

Q
Definitions : implies: P

Q, member: t

T, uall:

[x:A]. B[x], not:

A, false: False, prop:

Lemmas : not_wf
\mforall{}[P,Q:\mBbbP{}]. ((\mneg{}P) {}\mRightarrow{} P {}\mRightarrow{} Q) Date html generated: 2013_09_05-AM-11_12_31 Last ObjectModification: 2013_06_03-AM-11_00_48 Home Index