theorem Th35: :: HILBERT3:36

for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for p9 being Permutation of (SetVal (V,p))
for q9 being Permutation of (SetVal (V,q)) st p9 = Perm (P,p) & q9 = Perm (P,q) holds
Perm (P,(p => q)) = p9 => q9