Nuprl - Proof: implies functionality wrt iff

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

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

P2)

(Q1

Q2)

((P1

Q1)

(P2

Q2))

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