(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: contrapositive 1
1. P: Prop
2. Q: Prop
3. Dec(P)
4. Dec(Q)

(P Q) (Q P)
By:
UnfoldTopAb 3
THEN
UnfoldTopAb 4
Generated subgoal:

13. P P
4. Q Q
(P Q) (Q P)

About:
decidablepropimplies

(9steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc