Nuprl Lemma : logic3

[A,B,C:

]. ((A

B)

(B

C)

A

C)

Proof

Definitions occuring in Statement : uall:

[x:A]. B[x], prop:

, implies: P

Q
Definitions : prop:

, member: t

T, implies: P

Q
Lemmas : member_wf
\mforall{}[A,B,C:\mBbbP{}]. ((A {}\mRightarrow{} B) {}\mRightarrow{} (B {}\mRightarrow{} C) {}\mRightarrow{} A {}\mRightarrow{} C) Date html generated: 2013_09_05-AM-11_12_28 Last ObjectModification: 2013_06_24-AM-11_02_18 Home Index