(2steps total) PrintForm core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: or functionality wrt implies 1
1. P1 : Prop
2. P2 : Prop
3. Q1 : Prop
4. Q2 : Prop
5. P1  P2
6. Q1  Q2
7. P1  Q1
  P2  Q2
By: (Analyze 7 THENL [Sel 1 (Analyze 0);Sel 2 (Analyze 0)]) THEN HypBackchain

Generated subgoals:

None

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

(2steps total) PrintForm core StandardLIB Doc