Nuprl Lemma : logic8

[P,Q:

]. ((

(P

Q))

P

(

Q))

Proof

Definitions occuring in Statement : uall:

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

, not:

A, implies: P

Q
Definitions : prop:

, member: t

T, implies: P

Q, not:

A, uall:

[x:A]. B[x]
Lemmas : not_wf
\mforall{}[P,Q:\mBbbP{}]. ((\mneg{}(P {}\mRightarrow{} Q)) {}\mRightarrow{} P {}\mRightarrow{} (\mneg{}Q)) Date html generated: 2013_09_05-AM-11_12_55 Last ObjectModification: 2013_06_18-PM-01_43_57 Home Index