Nuprl Lemma : DeMorgan2

[P,Q:].  (((P  Q))  ((P)  (Q)))


Proof



Definitions occuring in Statement :  uall: [x:A]. B[x],  prop: ,  not: A,  implies: P  Q,  or: P  Q,  and: P  Q
Definitions :  uall: [x:A]. B[x],  member: t  T,  prop: ,  implies: P  Q,  and: P  Q,  not: A,  or: P  Q,  guard: {T}
Lemmas :  not_wf,  or_wf
\mforall{}[P,Q:\mBbbP{}].    ((\mneg{}(P  \mvee{}  Q))  {}\mRightarrow{}  ((\mneg{}P)  \mwedge{}  (\mneg{}Q)))


Date html generated: 2013_09_05-AM-11_13_21
Last ObjectModification: 2013_07_09-PM-01_26_28

Home Index