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 p => q = p1 => q1 by Th2;
hence ( p = p1 & q = q1 ) by Th11; :: thesis: verum