theorem :: VALUAT_1:43

for Al being QC-alphabet
for A being non empty set
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) by Th36;