theorem :: VALUAT_1:44

for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p & J |= p => q holds
J |= q