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

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

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

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

assume A2: M,v |= q => r ; :: thesis: M,v |= p => r

now :: thesis: ( M,v |= p implies M,v |= r )

assume M,v |= p ; :: thesis: M,v |= r
then M,v |= q by A1, ZF_MODEL:18;
hence M,v |= r by A2, ZF_MODEL:18; :: thesis: verum

end;

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

end;

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

end;

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