theorem :: ZF_LANG1:103

for p, q, r being ZF-formula
for M being non empty set st M |= p => q & M |= q => r holds
M |= p => r