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