let p, q, r be ZF-formula; :: thesis: for M being non empty set st M |= p => q & M |= q => r holds
M |= p => r
let M be non empty set ; :: thesis: ( M |= p => q & M |= q => r implies M |= p => r )
assume A1: ( M |= p => q & M |= q => r ) ; :: thesis: M |= p => r
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= p => r
( M,v |= p => q & M,v |= q => r ) by A1;
hence M,v |= p => r by Th102; :: thesis: verum