Nuprl - Proof: implies functionality wrt implies

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: implies functionality wrt implies

P1,P2,Q1,Q2:Prop. (P1

P2)

(Q1

Q2)

(P1

Q1)

By:	(Unfold `guard` 0 THEN GenUnivCD) THEN HypBackchain

Generated subgoals:

None

About:

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