let G1, G2, H1, H2 be ZF-formula; for x, y being Variable holds
( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
let x, y be Variable; ( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
( ( G1 = H1 / (x,y) & 'not' G2 = ('not' H2) / (x,y) ) iff G1 '&' ('not' G2) = (H1 '&' ('not' H2)) / (x,y) )
by Th158;
hence
( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
by Th156; verum