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