theorem Th16: :: LUKASI_1:16

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