let p, q, r be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => q) => ((p => r) => (p => (q '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) )
let M be non empty set ; :: thesis: for v being Function of VAR,M holds
( M,v |= (p => q) => ((p => r) => (p => (q '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) )
let v be Function of VAR,M; :: thesis: ( M,v |= (p => q) => ((p => r) => (p => (q '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) )

now :: thesis: for v being Function of VAR,M holds M,v |= (p => q) => ((p => r) => (p => (q '&' r)))

let v be Function of VAR,M; :: thesis: M,v |= (p => q) => ((p => r) => (p => (q '&' r)))

now :: thesis: ( M,v |= p => q implies M,v |= (p => r) => (p => (q '&' r)) )

assume A1: M,v |= p => q ; :: thesis: M,v |= (p => r) => (p => (q '&' r))

now :: thesis: ( M,v |= p => r implies M,v |= p => (q '&' r) )

assume M,v |= p => r ; :: thesis: M,v |= p => (q '&' r)
then ( M,v |= p implies ( M,v |= r & M,v |= q ) ) by A1, ZF_MODEL:18;
then ( M,v |= p implies M,v |= q '&' r ) by ZF_MODEL:15;
hence M,v |= p => (q '&' r) by ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= (p => r) => (p => (q '&' r)) by ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= (p => q) => ((p => r) => (p => (q '&' r))) by ZF_MODEL:18; :: thesis: verum

end;

hence ( M,v |= (p => q) => ((p => r) => (p => (q '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) ) ; :: thesis: verum