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 => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)) => ((p => q) => (p => r)) )
let M be non empty set ; :: thesis: for v being Function of VAR ,M holds
( M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)) => ((p => q) => (p => r)) )
let v be Function of VAR ,M; :: thesis: ( M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)) => ((p => q) => (p => r)) )

now

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

now

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

now

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

end;

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

end;

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

end;

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