I1.A->(B->A); I2.(A->(B->C))->((A->B)->(A->C)).
II1.(A& B)->A; II2.(A& B)->B; II3.(A->B)->((A->C)->(A->(B&C)).
III1.A->(BvA); III2.B->(AvB); III3.(A->C)->((B->C)->((AvB)->C)).
IV1.(A->B)->((not B)->(not A)); IV2.A->(not A); IV3.(not A)->A.
V1.VxF(x)->F(y); V2.F(y)->ЭxF(x).
