Nuprl Lemma : contrapos1

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 : member: t

T, false: False, not:

A, guard: {T}, implies: P

Q, prop:

, all:

x:A. B[x], 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_02 Last ObjectModification: 2013_03_07-PM-08_12_49 Home Index