theorem ded: :: PL_AXIOM:58

for A, B being Element of PL-WFF
for F being Subset of PL-WFF st F \/ {A} |- B holds
F |- A => B