Nuprl Lemma : contrapos

P,Q:

. ({P

Q}

{(

Q)

(

P)})

Proof

Definitions occuring in Statement : prop:

, guard: {T}, all:

x:A. B[x], not:

A, implies: P

Q
Definitions : all:

x:A. B[x], prop:

, implies: P

Q, guard: {T}, not:

A, false: False, member: t

T, 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_03_20-AM-09_45_00 Last ObjectModification: 2013_02_26-PM-02_42_31 Home Index