theorem Th102: :: ZF_LANG1:102

for p, q, r being ZF-formula
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