theorem :: PROCAL_1:58

for A being QC-alphabet
for p, q being Element of CQC-WFF A st (p '&' ('not' q)) => ('not' p) in TAUT A holds
p => q in TAUT A