Nuprl Lemma : logic2

[A,B,C:

]. ((A

B)

(A

B

C)

A

C)

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,C:\mBbbP{}]. ((A {}\mRightarrow{} B) {}\mRightarrow{} (A {}\mRightarrow{} B {}\mRightarrow{} C) {}\mRightarrow{} A {}\mRightarrow{} C) Date html generated: 2013_09_05-AM-11_12_24 Last ObjectModification: 2013_05_24-AM-10_16_33 Home Index