let p, q, r, s be Element of HP-WFF ; :: thesis: p '&' q <> r => s
p '&' q = <*2*> ^ (p ^ q) by FINSEQ_1:32;
then ( r => s = <*1*> ^ (r ^ s) & (p '&' q) . 1 = 2 ) by FINSEQ_1:32, FINSEQ_1:41;
hence p '&' q <> r => s by FINSEQ_1:41; :: thesis: verum