let A be non empty set ; :: thesis: for v being Element of Valuations_in A
for p, q, t being Element of CQC-WFF
for J being interpretation of A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let v be Element of Valuations_in A; :: thesis: for p, q, t being Element of CQC-WFF
for J being interpretation of A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let p, q, t be Element of CQC-WFF ; :: thesis: for J being interpretation of A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let J be interpretation of A; :: thesis: J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
thus (Valid ((p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))),J) . v = TRUE :: according to VALUAT_1:def 12 :: thesis: verum

proof

A1: p => q = 'not' (p '&' ('not' q)) by QC_LANG2:def 2;
('not' (q '&' t)) => ('not' (p '&' t)) = 'not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))) by QC_LANG2:def 2;
then A2: (Valid ((p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))),J) . v = (Valid ('not' (('not' (p '&' ('not' q))) '&' ('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))))))),J) . v by A1, QC_LANG2:def 2
.= 'not' ((Valid (('not' (p '&' ('not' q))) '&' ('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t))))))),J) . v) by Th20
.= 'not' (((Valid ('not' (p '&' ('not' q))),J) . v) '&' ((Valid ('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))))),J) . v)) by Th22 ;
A3: (Valid ('not' (p '&' ('not' q))),J) . v = 'not' ((Valid (p '&' ('not' q)),J) . v) by Th20
.= 'not' (((Valid p,J) . v) '&' ((Valid ('not' q),J) . v)) by Th22
.= 'not' (((Valid p,J) . v) '&' ('not' ((Valid q,J) . v))) by Th20 ;
(Valid ('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))))),J) . v = 'not' ((Valid ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t))))),J) . v) by Th20
.= 'not' ('not' ((Valid (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))),J) . v)) by Th20
.= ((Valid ('not' (q '&' t)),J) . v) '&' ((Valid ('not' ('not' (p '&' t))),J) . v) by Th22
.= ('not' ((Valid (q '&' t),J) . v)) '&' ((Valid ('not' ('not' (p '&' t))),J) . v) by Th20
.= ('not' ((Valid (q '&' t),J) . v)) '&' ('not' ((Valid ('not' (p '&' t)),J) . v)) by Th20
.= ('not' ((Valid (q '&' t),J) . v)) '&' ('not' ('not' ((Valid (p '&' t),J) . v))) by Th20
.= ('not' (((Valid q,J) . v) '&' ((Valid t,J) . v))) '&' ((Valid (p '&' t),J) . v) by Th22
.= ('not' (((Valid q,J) . v) '&' ((Valid t,J) . v))) '&' (((Valid p,J) . v) '&' ((Valid t,J) . v)) by Th22 ;
hence (Valid ((p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))),J) . v = TRUE by A2, A3, Lm2; :: thesis: verum

end;