(11steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc iff via so 1 2 1
1. A : Prop
2. B : Prop
3. C:Prop. ((A  B)  (B  A)  C)  C
  (A  B)  (B  A)  (A  B)
By: UnivCD

Generated subgoal:

1 4. A  B
5. B  A
  A  B
3 steps

About:
propimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(11steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc