theorem :: PL_AXIOM:32

for p, q being Element of PL-WFF holds (p '&' q) => p is tautology