let A be QC-alphabet ; :: thesis: for p, q, p1, q1 being Element of QC-WFF A st p => q = p1 => q1 holds
( p = p1 & q = q1 )
let p, q, p1, q1 be Element of QC-WFF A; :: 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 Th2; :: thesis: q = q1
'not' q = 'not' q1 by A1, Th2;
hence q = q1 by FINSEQ_1:33; :: thesis: verum