let A be non empty set ; :: thesis: for p, q being Element of CQC-WFF
for J being interpretation of A st J |= p & J |= p => q holds
J |= q
let p, q be Element of CQC-WFF ; :: thesis: for J being interpretation of A st J |= p & J |= p => q holds
J |= q
let J be interpretation of A; :: thesis: ( J |= p & J |= p => q implies J |= q )
assume that
A1: J |= p and
A2: J |= p => q ; :: thesis: J |= q

now

let v be Element of Valuations_in A; :: thesis: J,v |= q
( J,v |= p & J,v |= p => q ) by A1, A2, Def13;
hence J,v |= q by Th36; :: thesis: verum

end;

hence J |= q by Def13; :: thesis: verum