(2steps total) PrintForm Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: disjunct elim 1

1. P : Prop
2. Q : Prop
3. P  Q
4. P
  Q


By: Analyze-2


Generated subgoals:

None

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

(2steps total) PrintForm Definitions LogicSupplement Sections DiscrMathExt Doc