let p, q, p1, q1 be Element of QC-WFF ; :: thesis: ( p => q = p1 => q1 implies ( p = p1 & q = q1 ) )
assume p => q = p1 => q1 ; :: thesis: ( p = p1 & q = q1 )
then A1: p '&' ('not' q) = p1 '&' ('not' q1) by FINSEQ_1:33;
hence p = p1 by Th3; :: thesis: q = q1
'not' q = 'not' q1 by A1, Th3;
hence q = q1 by FINSEQ_1:33; :: thesis: verum