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