theorem :: LUKASI_1:17

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 & s in TAUT A holds
p in TAUT A