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
p => (q => X) is Element of CQC-WFF A
p => q 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
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 => (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 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 => (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
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
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
(p => q) => X is Element of CQC-WFF A
q => X is Element of CQC-WFF A
((p => q) => X) => (q => 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
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
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
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 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
'not' q is Element of CQC-WFF A
'not' p 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
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
'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
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
'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 valid Element of CQC-WFF A
(q => p) => (('not' p) => ('not' 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
'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
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
'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))
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 valid Element of CQC-WFF A
p => ('not' ('not' p)) 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
'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
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
'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 valid Element of CQC-WFF A
('not' ('not' p)) => p 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
'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
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
'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 valid Element of CQC-WFF A
q => ('not' ('not' 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
'not' q is Element of CQC-WFF A
p => ('not' q) is Element of CQC-WFF A
'not' p 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
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
'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 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
'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
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
'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 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
K6((CQC-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
X is Element of K6((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
K6((CQC-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
X is Element of K6((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
K6((CQC-WFF A)) is set
q is Element of K6((CQC-WFF A))
p is Element of CQC-WFF A
p => p 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
K6((CQC-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
X is Element of K6((CQC-WFF A))
p => (q => p) 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
K6((CQC-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
X is Element of K6((CQC-WFF A))
p => ((p => q) => 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
K6((CQC-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
X is Element of K6((CQC-WFF A))
(p => (q => X)) => (q => (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
K6((CQC-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
X is Element of K6((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
K6((CQC-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
X is Element of K6((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
K6((CQC-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
(p => q) => X is Element of CQC-WFF A
q => X is Element of CQC-WFF A
X is Element of K6((CQC-WFF A))
((p => q) => X) => (q => 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
K6((CQC-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 => (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
X is Element of K6((CQC-WFF A))
(p => (q => X)) => ((p => q) => (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
K6((CQC-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 => (q => X) is Element of CQC-WFF A
p => X is Element of CQC-WFF A
X is Element of K6((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
K6((CQC-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
q => p is Element of CQC-WFF A
X is Element of K6((CQC-WFF A))
(('not' p) => ('not' q)) => (q => p) is valid Element of CQC-WFF A
(q => p) => (('not' p) => ('not' 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
K6((CQC-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
q is Element of K6((CQC-WFF A))
('not' ('not' p)) => p is valid Element of CQC-WFF A
p => ('not' ('not' p)) 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
K6((CQC-WFF A)) is set
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
X is Element of K6((CQC-WFF A))
(p => ('not' ('not' q))) => (p => q) is valid Element of CQC-WFF A
q => ('not' ('not' 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
K6((CQC-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
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
X is Element of K6((CQC-WFF A))
(('not' ('not' p)) => q) => (p => q) is valid Element of CQC-WFF A
('not' ('not' p)) => p 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
K6((CQC-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
p => ('not' q) is Element of CQC-WFF A
q => ('not' p) is Element of CQC-WFF A
X is Element of K6((CQC-WFF A))
(p => ('not' q)) => (q => ('not' p)) 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
K6((CQC-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' 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
X is Element of K6((CQC-WFF A))
(('not' p) => q) => (('not' q) => p) 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
K6((CQC-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
p => ('not' q) is Element of CQC-WFF A
X is Element of K6((CQC-WFF A))
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
K6((CQC-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' p) => q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
X is Element of K6((CQC-WFF A))
('not' q) => p is Element of CQC-WFF A