:: LUKASI_1 semantic presentation

K32() is Element of K6(K28())

K28() is set

K6(K28()) is set

K27() is set

K6(K27()) is set

K6(K32()) is set

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(q => X) => (p => X) is Element of CQC-WFF A

(p => q) => ((q => X) => (p => X)) is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

q '&' ('not' X) is Element of CQC-WFF A

'not' (q '&' ('not' X)) is Element of CQC-WFF A

p '&' ('not' X) is Element of CQC-WFF A

'not' (p '&' ('not' X)) is Element of CQC-WFF A

('not' (q '&' ('not' X))) => ('not' (p '&' ('not' X))) is Element of CQC-WFF A

(p => q) => (('not' (q '&' ('not' X))) => ('not' (p '&' ('not' X)))) is Element of CQC-WFF A

(q => X) => ('not' (p '&' ('not' X))) is Element of CQC-WFF A

(p => q) => ((q => X) => ('not' (p '&' ('not' X)))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(q => X) => (p => X) is Element of CQC-WFF A

(p => q) => ((q => X) => (p => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(q => X) => (p => X) is Element of CQC-WFF A

(p => q) => ((q => X) => (p => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

p => p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

('not' p) => p is Element of CQC-WFF A

(('not' p) => p) => p is Element of CQC-WFF A

p => (('not' p) => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

X => q is Element of CQC-WFF A

(p => q) => (X => q) is Element of CQC-WFF A

X => p is Element of CQC-WFF A

X is Element of CQC-WFF A

((p => q) => (X => q)) => X is Element of CQC-WFF A

(X => p) => X is Element of CQC-WFF A

(((p => q) => (X => q)) => X) => ((X => p) => X) is Element of CQC-WFF A

(X => p) => ((p => q) => (X => q)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

X is Element of CQC-WFF A

X => q is Element of CQC-WFF A

X => X is Element of CQC-WFF A

p => (X => X) is Element of CQC-WFF A

(X => q) => (p => (X => X)) is Element of CQC-WFF A

(p => (q => X)) => ((X => q) => (p => (X => X))) is Element of CQC-WFF A

(q => X) => (X => X) is Element of CQC-WFF A

((q => X) => (X => X)) => (p => (X => X)) is Element of CQC-WFF A

(((q => X) => (X => X)) => (p => (X => X))) => ((X => q) => (p => (X => X))) is Element of CQC-WFF A

((((q => X) => (X => X)) => (p => (X => X))) => ((X => q) => (p => (X => X)))) => ((p => (q => X)) => ((X => q) => (p => (X => X)))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => X) => X is Element of CQC-WFF A

(q => X) => X is Element of CQC-WFF A

((p => X) => X) => ((q => X) => X) is Element of CQC-WFF A

(p => q) => (((p => X) => X) => ((q => X) => X)) is Element of CQC-WFF A

(q => X) => (p => X) is Element of CQC-WFF A

((q => X) => (p => X)) => (((p => X) => X) => ((q => X) => X)) is Element of CQC-WFF A

(((q => X) => (p => X)) => (((p => X) => X) => ((q => X) => X))) => ((p => q) => (((p => X) => X) => ((q => X) => X))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

X is Element of CQC-WFF A

(q => X) => X is Element of CQC-WFF A

p => ((q => X) => X) is Element of CQC-WFF A

q is Element of CQC-WFF A

q => q is Element of CQC-WFF A

q => X is Element of CQC-WFF A

(q => X) => X is Element of CQC-WFF A

p => ((q => X) => X) is Element of CQC-WFF A

(q => q) => (p => ((q => X) => X)) is Element of CQC-WFF A

(p => ((q => X) => X)) => ((q => q) => (p => ((q => X) => X))) is Element of CQC-WFF A

((q => X) => X) => ((q => X) => X) is Element of CQC-WFF A

(q => q) => (((q => X) => X) => ((q => X) => X)) is Element of CQC-WFF A

((q => q) => (((q => X) => X) => ((q => X) => X))) => ((p => ((q => X) => X)) => ((q => q) => (p => ((q => X) => X)))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(('not' p) => q) => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

((('not' p) => q) => X) => (p => X) is Element of CQC-WFF A

p => (('not' p) => q) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(('not' p) => q) => X is Element of CQC-WFF A

X is Element of CQC-WFF A

X => q is Element of CQC-WFF A

(X => q) => X is Element of CQC-WFF A

((('not' p) => q) => X) => ((X => q) => X) is Element of CQC-WFF A

p => (((('not' p) => q) => X) => ((X => q) => X)) is Element of CQC-WFF A

('not' p) => X is Element of CQC-WFF A

(('not' p) => X) => (((('not' p) => q) => X) => ((X => q) => X)) is Element of CQC-WFF A

((('not' p) => X) => (((('not' p) => q) => X) => ((X => q) => X))) => (p => (((('not' p) => q) => X) => ((X => q) => X))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => q is Element of CQC-WFF A

(('not' q) => q) => q is Element of CQC-WFF A

p => ((('not' q) => q) => q) is Element of CQC-WFF A

(p => ((('not' q) => q) => q)) => ((('not' q) => q) => q) is Element of CQC-WFF A

'not' ((('not' q) => q) => q) is Element of CQC-WFF A

('not' ((('not' q) => q) => q)) => ((('not' q) => q) => q) is Element of CQC-WFF A

(('not' ((('not' q) => q) => q)) => ((('not' q) => q) => q)) => ((('not' q) => q) => q) is Element of CQC-WFF A

((('not' ((('not' q) => q) => q)) => ((('not' q) => q) => q)) => ((('not' q) => q) => q)) => ((p => ((('not' q) => q) => q)) => ((('not' q) => q) => q)) is Element of CQC-WFF A

((('not' q) => q) => q) => (((('not' ((('not' q) => q) => q)) => ((('not' q) => q) => q)) => ((('not' q) => q) => q)) => ((p => ((('not' q) => q) => q)) => ((('not' q) => q) => q))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => q is Element of CQC-WFF A

(('not' q) => q) => q is Element of CQC-WFF A

p => ((('not' q) => q) => q) is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

('not' p) => ((('not' q) => q) => q) is Element of CQC-WFF A

(('not' p) => ((('not' q) => q) => q)) => ((('not' q) => q) => q) is Element of CQC-WFF A

((('not' p) => ((('not' q) => q) => q)) => ((('not' q) => q) => q)) => (p => ((('not' q) => q) => q)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

q => p is Element of CQC-WFF A

(q => p) => p is Element of CQC-WFF A

X is Element of CQC-WFF A

X => ((q => p) => p) is Element of CQC-WFF A

(('not' p) => q) => (X => ((q => p) => p)) is Element of CQC-WFF A

('not' p) => p is Element of CQC-WFF A

(('not' p) => p) => p is Element of CQC-WFF A

X => ((('not' p) => p) => p) is Element of CQC-WFF A

(X => ((('not' p) => p) => p)) => ((('not' p) => q) => (X => ((q => p) => p))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

(q => X) => X is Element of CQC-WFF A

p => ((q => X) => X) is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

('not' X) => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => ((q => X) => X)) => X is Element of CQC-WFF A

(('not' X) => q) => X is Element of CQC-WFF A

((p => ((q => X) => X)) => X) => ((('not' X) => q) => X) is Element of CQC-WFF A

(('not' X) => q) => (p => ((q => X) => X)) is Element of CQC-WFF A

((('not' X) => q) => (p => ((q => X) => X))) => (((p => ((q => X) => X)) => X) => ((('not' X) => q) => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

q => p is Element of CQC-WFF A

(q => p) => p is Element of CQC-WFF A

(('not' p) => q) => ((q => p) => p) is Element of CQC-WFF A

'not' ((q => p) => p) is Element of CQC-WFF A

('not' ((q => p) => p)) => ((q => p) => p) is Element of CQC-WFF A

(('not' ((q => p) => p)) => ((q => p) => p)) => ((q => p) => p) is Element of CQC-WFF A

((('not' ((q => p) => p)) => ((q => p) => p)) => ((q => p) => p)) => ((('not' p) => q) => ((q => p) => p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

q => p is Element of CQC-WFF A

(q => p) => p is Element of CQC-WFF A

p => ((q => p) => p) is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

(('not' p) => q) => ((q => p) => p) is Element of CQC-WFF A

((('not' p) => q) => ((q => p) => p)) => (p => ((q => p) => p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

q => p is Element of CQC-WFF A

p => (q => p) is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => p is Element of CQC-WFF A

(('not' q) => p) => p is Element of CQC-WFF A

p => ((('not' q) => p) => p) is Element of CQC-WFF A

q => (('not' q) => p) is Element of CQC-WFF A

(q => (('not' q) => p)) => (p => (q => p)) is Element of CQC-WFF A

(p => ((('not' q) => p) => p)) => ((q => (('not' q) => p)) => (p => (q => p))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => q) => X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

((p => q) => X) => (q => X) is Element of CQC-WFF A

q => (p => q) is Element of CQC-WFF A

(q => (p => q)) => (((p => q) => X) => (q => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

(p => q) => q is Element of CQC-WFF A

p => ((p => q) => q) is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => p is Element of CQC-WFF A

(('not' q) => p) => ((p => q) => q) is Element of CQC-WFF A

((('not' q) => p) => ((p => q) => q)) => (p => ((p => q) => q)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

q => (p => X) is Element of CQC-WFF A

(p => (q => X)) => (q => (p => X)) is Element of CQC-WFF A

(q => X) => X is Element of CQC-WFF A

q => ((q => X) => X) is Element of CQC-WFF A

(q => ((q => X) => X)) => ((p => (q => X)) => (q => (p => X))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

X => p is Element of CQC-WFF A

X => q is Element of CQC-WFF A

(X => p) => (X => q) is Element of CQC-WFF A

(p => q) => ((X => p) => (X => q)) is Element of CQC-WFF A

(p => q) => (X => q) is Element of CQC-WFF A

(X => p) => ((p => q) => (X => q)) is Element of CQC-WFF A

((X => p) => ((p => q) => (X => q))) => ((p => q) => ((X => p) => (X => q))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

q => (p => X) is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => (q => X)) => X is Element of CQC-WFF A

(q => (p => X)) => X is Element of CQC-WFF A

((p => (q => X)) => X) => ((q => (p => X)) => X) is Element of CQC-WFF A

(q => (p => X)) => (p => (q => X)) is Element of CQC-WFF A

((q => (p => X)) => (p => (q => X))) => (((p => (q => X)) => X) => ((q => (p => X)) => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

(p => q) => p is Element of CQC-WFF A

((p => q) => p) => p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

('not' p) => (p => q) is Element of CQC-WFF A

(('not' p) => (p => q)) => (((p => q) => p) => p) is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

p => (('not' p) => q) is Element of CQC-WFF A

(p => (('not' p) => q)) => (((p => q) => p) => p) is Element of CQC-WFF A

((('not' p) => (p => q)) => (((p => q) => p) => p)) => ((p => (('not' p) => q)) => (((p => q) => p) => p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => q) => X is Element of CQC-WFF A

X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

X => q is Element of CQC-WFF A

(X => q) => X is Element of CQC-WFF A

(p => X) => ((X => q) => X) is Element of CQC-WFF A

((p => q) => X) => ((p => X) => ((X => q) => X)) is Element of CQC-WFF A

((p => q) => X) => ((X => q) => X) is Element of CQC-WFF A

(p => X) => (((p => q) => X) => ((X => q) => X)) is Element of CQC-WFF A

((p => X) => (((p => q) => X) => ((X => q) => X))) => (((p => q) => X) => ((p => X) => ((X => q) => X))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => q) => X is Element of CQC-WFF A

X => p is Element of CQC-WFF A

(X => p) => p is Element of CQC-WFF A

((p => q) => X) => ((X => p) => p) is Element of CQC-WFF A

(p => q) => p is Element of CQC-WFF A

((p => q) => p) => p is Element of CQC-WFF A

(((p => q) => p) => p) => (((p => q) => X) => ((X => p) => p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

(p => q) => q is Element of CQC-WFF A

X is Element of CQC-WFF A

((p => q) => q) => X is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

(q => X) => p is Element of CQC-WFF A

((q => X) => p) => X is Element of CQC-WFF A

(((p => q) => q) => X) => (((q => X) => p) => X) is Element of CQC-WFF A

((q => X) => p) => ((p => q) => q) is Element of CQC-WFF A

(((q => X) => p) => ((p => q) => q)) => ((((p => q) => q) => X) => (((q => X) => p) => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => q) => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(p => X) => X is Element of CQC-WFF A

((p => q) => X) => ((p => X) => X) is Element of CQC-WFF A

X => p is Element of CQC-WFF A

(X => p) => p is Element of CQC-WFF A

((X => p) => p) => ((p => X) => X) is Element of CQC-WFF A

(((X => p) => p) => ((p => X) => X)) => (((p => q) => X) => ((p => X) => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

p => (p => q) is Element of CQC-WFF A

(p => (p => q)) => (p => q) is Element of CQC-WFF A

(p => q) => (p => q) is Element of CQC-WFF A

((p => q) => (p => q)) => ((p => (p => q)) => (p => q)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => X) => X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

(q => X) => X is Element of CQC-WFF A

((p => X) => X) => ((q => X) => X) is Element of CQC-WFF A

(p => q) => (((p => X) => X) => ((q => X) => X)) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(p => X) => X is Element of CQC-WFF A

((p => X) => X) => ((p => X) => X) is Element of CQC-WFF A

(((p => X) => X) => ((p => X) => X)) => ((p => q) => (((p => X) => X) => ((q => X) => X))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

(p => q) => X is Element of CQC-WFF A

X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

X => X is Element of CQC-WFF A

(X => X) => X is Element of CQC-WFF A

(p => X) => ((X => X) => X) is Element of CQC-WFF A

((p => q) => X) => ((p => X) => ((X => X) => X)) is Element of CQC-WFF A

((p => q) => X) => ((X => X) => X) is Element of CQC-WFF A

(p => X) => (((p => q) => X) => ((X => X) => X)) is Element of CQC-WFF A

((p => X) => (((p => q) => X) => ((X => X) => X))) => (((p => q) => X) => ((p => X) => ((X => X) => X))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

X => (p => X) is Element of CQC-WFF A

q => (X => (p => X)) is Element of CQC-WFF A

(q => (X => (p => X))) => (X => (p => X)) is Element of CQC-WFF A

(p => q) => ((q => (X => (p => X))) => (X => (p => X))) is Element of CQC-WFF A

(p => X) => (X => (p => X)) is Element of CQC-WFF A

((p => X) => (X => (p => X))) => ((p => q) => ((q => (X => (p => X))) => (X => (p => X)))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

X => p is Element of CQC-WFF A

X is Element of CQC-WFF A

X => X is Element of CQC-WFF A

q => (X => X) is Element of CQC-WFF A

p => (q => (X => X)) is Element of CQC-WFF A

(X => p) => (q => (X => X)) is Element of CQC-WFF A

(p => (q => (X => X))) => ((X => p) => (q => (X => X))) is Element of CQC-WFF A

(p => (q => (X => X))) => (q => (X => X)) is Element of CQC-WFF A

(X => p) => ((p => (q => (X => X))) => (q => (X => X))) is Element of CQC-WFF A

((X => p) => ((p => (q => (X => X))) => (q => (X => X)))) => ((p => (q => (X => X))) => ((X => p) => (q => (X => X)))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(p => q) => (p => X) is Element of CQC-WFF A

(p => (q => X)) => ((p => q) => (p => X)) is Element of CQC-WFF A

(q => X) => ((p => q) => (p => X)) is Element of CQC-WFF A

((q => X) => ((p => q) => (p => X))) => ((p => (q => X)) => ((p => q) => (p => X))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

('not' (VERUM A)) => p is Element of CQC-WFF A

(VERUM A) => (('not' (VERUM A)) => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

q => p is Element of CQC-WFF A

p => (q => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

(p => q) => q is Element of CQC-WFF A

p => ((p => q) => q) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

q => (p => X) is Element of CQC-WFF A

(p => (q => X)) => (q => (p => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

q => (p => X) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

p => (p => q) is Element of CQC-WFF A

(p => (p => q)) => (p => q) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(p => q) => (p => X) is Element of CQC-WFF A

(p => (q => X)) => ((p => q) => (p => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(p => q) => (p => X) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

X is Element of CQC-WFF A

X => X is Element of CQC-WFF A

p => (X => X) is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

(X => X) => (q => X) is Element of CQC-WFF A

(q => X) => ((X => X) => (q => X)) is Element of CQC-WFF A

p => ((q => X) => ((X => X) => (q => X))) is Element of CQC-WFF A

p => ((X => X) => (q => X)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

VERUM A is Element of CQC-WFF A

p => (VERUM A) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

p => ('not' (VERUM A)) is Element of CQC-WFF A

('not' p) => (p => ('not' (VERUM A))) is Element of CQC-WFF A

('not' p) => ('not' (VERUM A)) is Element of CQC-WFF A

p => (('not' p) => ('not' (VERUM A))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

('not' p) => ('not' (VERUM A)) is Element of CQC-WFF A

(('not' p) => ('not' (VERUM A))) => p is Element of CQC-WFF A

('not' (VERUM A)) => p is Element of CQC-WFF A

('not' p) => (('not' (VERUM A)) => p) is Element of CQC-WFF A

('not' p) => p is Element of CQC-WFF A

(('not' p) => ('not' (VERUM A))) => (('not' p) => p) is Element of CQC-WFF A

(('not' p) => (('not' (VERUM A)) => p)) => ((('not' p) => ('not' (VERUM A))) => (('not' p) => p)) is Element of CQC-WFF A

(('not' p) => p) => p is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' p) => ('not' q) is Element of CQC-WFF A

q => p is Element of CQC-WFF A

(('not' p) => ('not' q)) => (q => p) is Element of CQC-WFF A

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

('not' q) => ('not' (VERUM A)) is Element of CQC-WFF A

q => (('not' q) => ('not' (VERUM A))) is Element of CQC-WFF A

('not' p) => ('not' (VERUM A)) is Element of CQC-WFF A

(('not' p) => ('not' q)) => (('not' p) => ('not' (VERUM A))) is Element of CQC-WFF A

(('not' q) => ('not' (VERUM A))) => ((('not' p) => ('not' q)) => (('not' p) => ('not' (VERUM A)))) is Element of CQC-WFF A

q => ((('not' p) => ('not' q)) => (('not' p) => ('not' (VERUM A)))) is Element of CQC-WFF A

(('not' p) => ('not' (VERUM A))) => p is Element of CQC-WFF A

q => ((('not' p) => ('not' (VERUM A))) => p) is Element of CQC-WFF A

(('not' p) => ('not' q)) => p is Element of CQC-WFF A

q => ((('not' p) => ('not' q)) => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

('not' ('not' p)) => p is Element of CQC-WFF A

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

('not' p) => ('not' (VERUM A)) is Element of CQC-WFF A

('not' ('not' p)) => (('not' p) => ('not' (VERUM A))) is Element of CQC-WFF A

(VERUM A) => p is Element of CQC-WFF A

(('not' p) => ('not' (VERUM A))) => ((VERUM A) => p) is Element of CQC-WFF A

('not' ('not' p)) => ((VERUM A) => p) is Element of CQC-WFF A

(VERUM A) => (('not' ('not' p)) => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

('not' ('not' p)) => p is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

p => ('not' (VERUM A)) is Element of CQC-WFF A

('not' ('not' p)) => ('not' (VERUM A)) is Element of CQC-WFF A

(p => ('not' (VERUM A))) => (('not' ('not' p)) => ('not' (VERUM A))) is Element of CQC-WFF A

(('not' ('not' p)) => ('not' (VERUM A))) => ('not' p) is Element of CQC-WFF A

(p => ('not' (VERUM A))) => ('not' p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => ('not' p) is Element of CQC-WFF A

(p => q) => (('not' q) => ('not' p)) is Element of CQC-WFF A

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

q => ('not' (VERUM A)) is Element of CQC-WFF A

('not' q) => (q => ('not' (VERUM A))) is Element of CQC-WFF A

p => ('not' (VERUM A)) is Element of CQC-WFF A

(p => q) => (p => ('not' (VERUM A))) is Element of CQC-WFF A

(q => ('not' (VERUM A))) => ((p => q) => (p => ('not' (VERUM A)))) is Element of CQC-WFF A

('not' q) => ((p => q) => (p => ('not' (VERUM A)))) is Element of CQC-WFF A

(p => ('not' (VERUM A))) => ('not' p) is Element of CQC-WFF A

('not' q) => ((p => ('not' (VERUM A))) => ('not' p)) is Element of CQC-WFF A

(p => q) => ('not' p) is Element of CQC-WFF A

('not' q) => ((p => q) => ('not' p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

p => ('not' ('not' p)) is Element of CQC-WFF A

VERUM A is Element of CQC-WFF A

(VERUM A) => p is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

('not' p) => ('not' (VERUM A)) is Element of CQC-WFF A

((VERUM A) => p) => (('not' p) => ('not' (VERUM A))) is Element of CQC-WFF A

(('not' p) => ('not' (VERUM A))) => ('not' ('not' p)) is Element of CQC-WFF A

((VERUM A) => p) => ('not' ('not' p)) is Element of CQC-WFF A

p => ((VERUM A) => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

q is Element of CQC-WFF A

('not' ('not' p)) => q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

(('not' ('not' p)) => q) => (p => q) is Element of CQC-WFF A

(p => q) => (('not' ('not' p)) => q) is Element of CQC-WFF A

p => ('not' ('not' p)) is Element of CQC-WFF A

('not' ('not' p)) => p is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

'not' ('not' q) is Element of CQC-WFF A

p => ('not' ('not' q)) is Element of CQC-WFF A

p => q is Element of CQC-WFF A

(p => ('not' ('not' q))) => (p => q) is Element of CQC-WFF A

(p => q) => (p => ('not' ('not' q))) is Element of CQC-WFF A

('not' ('not' q)) => q is Element of CQC-WFF A

p => (('not' ('not' q)) => q) is Element of CQC-WFF A

(p => (('not' ('not' q)) => q)) => ((p => ('not' ('not' q))) => (p => q)) is Element of CQC-WFF A

q => ('not' ('not' q)) is Element of CQC-WFF A

p => (q => ('not' ('not' q))) is Element of CQC-WFF A

(p => (q => ('not' ('not' q)))) => ((p => q) => (p => ('not' ('not' q)))) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

p => ('not' q) is Element of CQC-WFF A

q => ('not' p) is Element of CQC-WFF A

(p => ('not' q)) => (q => ('not' p)) is Element of CQC-WFF A

'not' ('not' q) is Element of CQC-WFF A

('not' ('not' q)) => ('not' p) is Element of CQC-WFF A

(p => ('not' q)) => (('not' ('not' q)) => ('not' p)) is Element of CQC-WFF A

(('not' ('not' q)) => ('not' p)) => (q => ('not' p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => p is Element of CQC-WFF A

(('not' p) => q) => (('not' q) => p) is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

('not' q) => ('not' ('not' p)) is Element of CQC-WFF A

(('not' p) => q) => (('not' q) => ('not' ('not' p))) is Element of CQC-WFF A

(('not' q) => ('not' ('not' p))) => (('not' q) => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

p => ('not' p) is Element of CQC-WFF A

(p => ('not' p)) => ('not' p) is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

('not' ('not' p)) => ('not' p) is Element of CQC-WFF A

(('not' ('not' p)) => ('not' p)) => ('not' p) is Element of CQC-WFF A

(p => ('not' p)) => (('not' ('not' p)) => ('not' p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

('not' p) => (p => q) is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

('not' ('not' p)) => q is Element of CQC-WFF A

('not' p) => (('not' ('not' p)) => q) is Element of CQC-WFF A

(('not' ('not' p)) => q) => (p => q) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => ('not' p) is Element of CQC-WFF A

(p => q) => (('not' q) => ('not' p)) is Element of CQC-WFF A

(('not' q) => ('not' p)) => (p => q) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' p) => ('not' q) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

q => p is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

p => ('not' ('not' p)) is Element of CQC-WFF A

('not' ('not' p)) => p is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

'not' ('not' q) is Element of CQC-WFF A

p => ('not' ('not' q)) is Element of CQC-WFF A

(p => q) => (p => ('not' ('not' q))) is Element of CQC-WFF A

(p => ('not' ('not' q))) => (p => q) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

'not' ('not' p) is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

('not' ('not' p)) => q is Element of CQC-WFF A

(p => q) => (('not' ('not' p)) => q) is Element of CQC-WFF A

(('not' ('not' p)) => q) => (p => q) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

p => ('not' q) is Element of CQC-WFF A

q => ('not' p) is Element of CQC-WFF A

(p => ('not' q)) => (q => ('not' p)) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

p is Element of CQC-WFF A

'not' p is Element of CQC-WFF A

q is Element of CQC-WFF A

('not' p) => q is Element of CQC-WFF A

'not' q is Element of CQC-WFF A

('not' q) => p is Element of CQC-WFF A

(('not' p) => q) => (('not' q) => p) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(q => X) => (p => X) is Element of CQC-WFF A

(p => q) => ((q => X) => (p => X)) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

(q => X) => (p => X) is Element of CQC-WFF A

(p => q) => ((q => X) => (p => X)) is valid Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => X is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

p => p is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

q => p is Element of CQC-WFF A

p => (q => p) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

q => p is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

X is Element of CQC-WFF A

q is Element of CQC-WFF A

p is Element of CQC-WFF A

q => p is Element of CQC-WFF A

X => (q => p) is Element of CQC-WFF A

X => p is Element of CQC-WFF A

q => (X => p) is Element of CQC-WFF A

(X => (q => p)) => (q => (X => p)) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

q => (p => X) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A

p => (q => X) is Element of CQC-WFF A

p => X is Element of CQC-WFF A

q => (p => X) is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

VERUM A is Element of CQC-WFF A

'not' (VERUM A) is Element of CQC-WFF A

p is Element of CQC-WFF A

p => (VERUM A) is Element of CQC-WFF A

('not' (VERUM A)) => p is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

(p => q) => q is Element of CQC-WFF A

p => ((p => q) => q) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

p => (p => q) is Element of CQC-WFF A

(p => (p => q)) => (p => q) is Element of CQC-WFF A

TAUT A is Element of K6((CQC-WFF A))

K6((CQC-WFF A)) is set

K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

Cn K10((CQC-WFF A)) is Element of K6((CQC-WFF A))

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

p => q is Element of CQC-WFF A

p => (p => q) is Element of CQC-WFF A

(p => (p => q)) => (p => q) is valid Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is V1() set

CQC-WFF A is V1() Element of K6((QC-WFF A))

K6((QC-WFF A)) is set

p is Element of CQC-WFF A

q is Element of CQC-WFF A

X is Element of CQC-WFF A

q => X is Element of CQC-WFF A