let G1, G2, H1, H2 be ZF-formula; :: thesis: 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; :: thesis: ( G1 '&' G2 = (H1 '&' H2) / x,y iff ( G1 = H1 / x,y & G2 = H2 / x,y ) )
thus ( G1 '&' G2 = (H1 '&' H2) / x,y implies ( G1 = H1 / x,y & G2 = H2 / x,y ) ) :: thesis: ( G1 = H1 / x,y & G2 = H2 / x,y implies G1 '&' G2 = (H1 '&' H2) / x,y )

proof

assume G1 '&' G2 = (H1 '&' H2) / x,y ; :: thesis: ( G1 = H1 / x,y & G2 = H2 / x,y )
then G1 '&' G2 = (H1 / x,y) '&' (H2 / x,y) by Lm1;
hence ( G1 = H1 / x,y & G2 = H2 / x,y ) by ZF_LANG:47; :: thesis: verum

end;

thus ( G1 = H1 / x,y & G2 = H2 / x,y implies G1 '&' G2 = (H1 '&' H2) / x,y ) by Lm1; :: thesis: verum