Nuprl Lemma : logic1

[A,B:].  (A  B  A)


Proof



Definitions occuring in Statement :  uall: [x:A]. B[x],  prop: ,  implies: P  Q
Definitions :  uall: [x:A]. B[x],  member: t  T,  prop: ,  implies: P  Q
Lemmas :  member_wf
\mforall{}[A,B:\mBbbP{}].    (A  {}\mRightarrow{}  B  {}\mRightarrow{}  A)


Date html generated: 2013_09_05-AM-11_12_17
Last ObjectModification: 2013_05_24-AM-10_04_00

Home Index