3 (`!a b c. a /\ b ==> c <=> a ==> b ==> c`,CONV_TAC TAUT);;
5 (`!a b c. a /\ b ==> c <=> (a<=>T) ==> b ==> c`,CONV_TAC TAUT);;
7 (`!a b c. ~a /\ b ==> c <=> (a<=>F) ==> b ==> c`,CONV_TAC TAUT);;
9 let NOT_NOT = GEN_ALL (hd (CONJUNCTS (SPEC_ALL NOT_CLAUSES)));;
12 (`!a. (~a /\ a) <=> F`,CONV_TAC TAUT);;
14 let AND_INV_IMP = prove
15 (`!a. a ==> ~a ==> F`,CONV_TAC TAUT);;
18 (`(~(a \/ b) ==> F) = (~a ==> ~b ==> F)`,CONV_TAC TAUT);;
21 (`(~(a \/ b) ==> F) = ((a==>F) ==> ~b ==> F)`,CONV_TAC TAUT);;
24 (`(~(~a \/ b) ==> F) = (a ==> ~b ==> F)`,CONV_TAC TAUT);;
27 (`(~a ==> F) ==> (a==>F) ==> F`,CONV_TAC TAUT)
30 (`(~a ==> F) <=> a`,CONV_TAC TAUT)
32 let IMP_F_EQ_F = prove
33 (`!t. (t ==> F) <=> (t <=> F)`,CONV_TAC TAUT);;