let p, q be Element of HP-WFF ; :: thesis: (p '&' q) => p is pseudo-canonical
reconsider s = (p '&' q) => p as canonical Element of HP-WFF by Th43;
s is pseudo-canonical ;
hence (p '&' q) => p is pseudo-canonical ; :: thesis: verum