Nuprl Lemma : logic6

Nuprl Lemma : logic6_contrapos

[P,Q:

]. ((P

Q)

(

Q)

(

P))

Proof

Definitions occuring in Statement : uall:

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

, not:

A, implies: P

Q
Definitions : implies: P

Q, member: t

T, prop:

, not:

A, uall:

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