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
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
p '&' ('not' p) is Element of CQC-WFF A
'not' (p '&' ('not' p)) is Element of CQC-WFF A
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
q is Element of CQC-WFF A
p 'or' 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' p) '&' ('not' q) is Element of CQC-WFF A
'not' (('not' p) '&' ('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
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
p 'or' ('not' p) is Element of CQC-WFF A
('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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
p => (p 'or' q) is Element of CQC-WFF A
'not' 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
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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
q 'or' p is Element of CQC-WFF A
p => (q 'or' p) is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' q) => p is Element of CQC-WFF A
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
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
('not' p) => q is Element of CQC-WFF A
(p 'or' q) => (('not' p) => q) is Element of CQC-WFF A
(('not' p) => q) => (('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
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
'not' (p 'or' 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
('not' (p 'or' q)) => (('not' p) '&' ('not' q)) is Element of CQC-WFF A
'not' (('not' p) '&' ('not' q)) is Element of CQC-WFF A
'not' ('not' (('not' p) '&' ('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
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
p 'or' q is Element of CQC-WFF A
'not' (p 'or' q) is Element of CQC-WFF A
(('not' p) '&' ('not' q)) => ('not' (p 'or' q)) is Element of CQC-WFF A
'not' (('not' p) '&' ('not' q)) is Element of CQC-WFF A
'not' ('not' (('not' p) '&' ('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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
q 'or' p is Element of CQC-WFF A
(p 'or' q) => (q 'or' 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' 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
(p 'or' 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
TAUT A is Element of K6((CQC-WFF A))
K6((CQC-WFF A)) is set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
('not' p) 'or' p is Element of CQC-WFF A
p 'or' ('not' p) is Element of CQC-WFF A
(p 'or' ('not' p)) => (('not' p) 'or' 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
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
'not' (p 'or' q) is Element of CQC-WFF A
('not' (p 'or' q)) => ('not' p) is Element of CQC-WFF A
p => (p 'or' q) is Element of CQC-WFF A
(p => (p 'or' q)) => (('not' (p 'or' 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
p is Element of CQC-WFF A
p 'or' p is Element of CQC-WFF A
(p 'or' 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
(p 'or' p) => (('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
p is Element of CQC-WFF A
p 'or' p is Element of CQC-WFF A
p => (p 'or' p) is Element of CQC-WFF A
TAUT A is Element of K6((CQC-WFF A))
K6((CQC-WFF A)) 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
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
p '&' ('not' p) is Element of CQC-WFF A
q is Element of CQC-WFF A
(p '&' ('not' p)) => q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
'not' (p '&' ('not' p)) is Element of CQC-WFF A
('not' q) => ('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
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) 'or' q is Element of CQC-WFF A
(p => q) => (('not' p) 'or' q) 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
('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)) => p) => ((p => q) => (('not' ('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
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
p => ('not' ('not' p)) is Element of CQC-WFF A
'not' (('not' ('not' p)) '&' q) is Element of CQC-WFF A
'not' (p '&' q) is Element of CQC-WFF A
('not' (('not' ('not' p)) '&' q)) => ('not' (p '&' q)) is Element of CQC-WFF A
(p => ('not' ('not' p))) => (('not' (('not' ('not' p)) '&' q)) => ('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
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
('not' ('not' p)) => p is Element of CQC-WFF A
'not' (p '&' q) is Element of CQC-WFF A
'not' (('not' ('not' p)) '&' q) is Element of CQC-WFF A
('not' (p '&' q)) => ('not' (('not' ('not' p)) '&' q)) is Element of CQC-WFF A
(('not' ('not' p)) => p) => (('not' (p '&' q)) => ('not' (('not' ('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
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
p => ('not' q) is Element of CQC-WFF A
'not' (p => ('not' q)) is Element of CQC-WFF A
(p '&' q) => ('not' (p => ('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
'not' (p '&' ('not' ('not' q))) is Element of CQC-WFF A
'not' ('not' (p '&' ('not' ('not' q)))) is Element of CQC-WFF A
(p '&' ('not' ('not' q))) => ('not' ('not' (p '&' ('not' ('not' q))))) is Element of CQC-WFF A
q '&' p is Element of CQC-WFF A
('not' ('not' q)) '&' p is Element of CQC-WFF A
(q '&' p) => (('not' ('not' q)) '&' p) is Element of CQC-WFF A
(p '&' q) => (q '&' p) is Element of CQC-WFF A
(p '&' q) => (('not' ('not' q)) '&' p) is Element of CQC-WFF A
(('not' ('not' q)) '&' p) => (p '&' ('not' ('not' q))) is Element of CQC-WFF A
(p '&' q) => (p '&' ('not' ('not' q))) is Element of CQC-WFF A
(p '&' q) => ('not' ('not' (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
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 => ('not' q)) is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
('not' (p => ('not' q))) => (p '&' 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
'not' (p '&' ('not' ('not' q))) is Element of CQC-WFF A
'not' ('not' (p '&' ('not' ('not' q)))) is Element of CQC-WFF A
('not' ('not' (p '&' ('not' ('not' q))))) => (p '&' ('not' ('not' q))) is Element of CQC-WFF A
('not' ('not' q)) '&' p is Element of CQC-WFF A
(p '&' ('not' ('not' q))) => (('not' ('not' q)) '&' p) is Element of CQC-WFF A
q '&' p is Element of CQC-WFF A
(('not' ('not' q)) '&' p) => (q '&' p) is Element of CQC-WFF A
(p '&' ('not' ('not' q))) => (q '&' p) is Element of CQC-WFF A
(q '&' p) => (p '&' q) is Element of CQC-WFF A
(p '&' ('not' ('not' q))) => (p '&' q) is Element of CQC-WFF A
('not' ('not' (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
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 '&' q) is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' p) 'or' ('not' q) is Element of CQC-WFF A
('not' (p '&' q)) => (('not' p) 'or' ('not' q)) 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
p => ('not' q) is Element of CQC-WFF A
('not' ('not' p)) => ('not' q) is Element of CQC-WFF A
(p => ('not' q)) => (('not' ('not' p)) => ('not' q)) is Element of CQC-WFF A
(('not' ('not' p)) => p) => ((p => ('not' q)) => (('not' ('not' p)) => ('not' q))) is Element of CQC-WFF A
'not' (p => ('not' q)) is Element of CQC-WFF A
('not' (p => ('not' q))) => (p '&' q) is Element of CQC-WFF A
'not' ('not' (p => ('not' q))) is Element of CQC-WFF A
('not' (p '&' q)) => ('not' ('not' (p => ('not' q)))) is Element of CQC-WFF A
('not' ('not' (p => ('not' q)))) => (p => ('not' q)) is Element of CQC-WFF A
('not' (p '&' q)) => (p => ('not' q)) is Element of CQC-WFF A
('not' (p '&' q)) => (('not' ('not' p)) => ('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
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) 'or' ('not' q) is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
'not' (p '&' q) is Element of CQC-WFF A
(('not' p) 'or' ('not' q)) => ('not' (p '&' q)) 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)) => ('not' q) is Element of CQC-WFF A
p => ('not' q) is Element of CQC-WFF A
(('not' ('not' p)) => ('not' q)) => (p => ('not' q)) is Element of CQC-WFF A
(p => ('not' ('not' p))) => ((('not' ('not' p)) => ('not' q)) => (p => ('not' q))) is Element of CQC-WFF A
'not' (p => ('not' q)) is Element of CQC-WFF A
(p '&' q) => ('not' (p => ('not' q))) is Element of CQC-WFF A
'not' ('not' (p => ('not' q))) is Element of CQC-WFF A
('not' ('not' (p => ('not' q)))) => ('not' (p '&' q)) is Element of CQC-WFF A
(p => ('not' q)) => ('not' ('not' (p => ('not' q)))) is Element of CQC-WFF A
(p => ('not' q)) => ('not' (p '&' q)) is Element of CQC-WFF A
(('not' p) 'or' ('not' q)) => (p => ('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
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
'not' p is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' p) 'or' ('not' q) is Element of CQC-WFF A
('not' p) => (('not' p) 'or' ('not' q)) is Element of CQC-WFF A
'not' (('not' p) 'or' ('not' q)) is Element of CQC-WFF A
'not' ('not' p) is Element of CQC-WFF A
('not' (('not' p) 'or' ('not' q))) => ('not' ('not' p)) is Element of CQC-WFF A
'not' (p '&' q) is Element of CQC-WFF A
(('not' p) 'or' ('not' q)) => ('not' (p '&' q)) is Element of CQC-WFF A
'not' ('not' (p '&' q)) is Element of CQC-WFF A
('not' ('not' (p '&' q))) => ('not' (('not' p) 'or' ('not' q))) is Element of CQC-WFF A
(p '&' q) => ('not' ('not' (p '&' q))) is Element of CQC-WFF A
(p '&' q) => ('not' (('not' p) 'or' ('not' q))) is Element of CQC-WFF A
('not' ('not' p)) => p is Element of CQC-WFF A
('not' (('not' p) 'or' ('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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
(p '&' q) => (p 'or' q) is Element of CQC-WFF A
p => (p 'or' q) 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
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
q '&' p is Element of CQC-WFF A
(q '&' p) => q is Element of CQC-WFF A
(p '&' q) => (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
p is Element of CQC-WFF A
p '&' p is Element of CQC-WFF A
p => (p '&' p) is Element of CQC-WFF A
'not' (p '&' p) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
('not' p) 'or' ('not' p) is Element of CQC-WFF A
('not' (p '&' p)) => (('not' p) 'or' ('not' p)) is Element of CQC-WFF A
(('not' p) 'or' ('not' p)) => ('not' p) is Element of CQC-WFF A
('not' (p '&' 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p <=> q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
(p <=> q) => (p => q) is Element of CQC-WFF A
q => p is Element of CQC-WFF A
(p => q) '&' (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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p <=> q is Element of CQC-WFF A
q => p is Element of CQC-WFF A
(p <=> q) => (q => p) is Element of CQC-WFF A
p => q is Element of CQC-WFF A
(p => q) '&' (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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
r is Element of CQC-WFF A
(p 'or' q) 'or' r is Element of CQC-WFF A
q 'or' r is Element of CQC-WFF A
p 'or' (q 'or' r) is Element of CQC-WFF A
((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
('not' r) => q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' q) => r is Element of CQC-WFF A
(('not' r) => q) => (('not' q) => r) is Element of CQC-WFF A
('not' p) => ((('not' r) => q) => (('not' q) => r)) is Element of CQC-WFF A
('not' p) => (('not' r) => q) is Element of CQC-WFF A
('not' p) => (('not' q) => r) is Element of CQC-WFF A
(('not' p) => (('not' r) => q)) => (('not' p) => (('not' q) => r)) is Element of CQC-WFF A
(('not' p) => ((('not' r) => q) => (('not' q) => r))) => ((('not' p) => (('not' r) => q)) => (('not' p) => (('not' q) => r))) is Element of CQC-WFF A
r 'or' (p 'or' q) is Element of CQC-WFF A
((p 'or' q) 'or' r) => (r 'or' (p 'or' q)) is Element of CQC-WFF A
('not' r) => (p 'or' q) is Element of CQC-WFF A
(r 'or' (p 'or' q)) => (('not' r) => (p 'or' q)) is Element of CQC-WFF A
((p 'or' q) 'or' r) => (('not' r) => (p 'or' q)) is Element of CQC-WFF A
('not' p) => q is Element of CQC-WFF A
('not' r) => (('not' p) => q) is Element of CQC-WFF A
((p 'or' q) 'or' r) => (('not' r) => (('not' p) => q)) is Element of CQC-WFF A
(('not' r) => (('not' p) => q)) => (('not' p) => (('not' r) => q)) is Element of CQC-WFF A
((p 'or' q) 'or' r) => (('not' p) => (('not' r) => q)) is Element of CQC-WFF A
((p 'or' q) 'or' r) => (('not' p) => (('not' q) => r)) is Element of CQC-WFF A
('not' p) => (q 'or' r) is Element of CQC-WFF A
((p 'or' q) 'or' r) => (('not' p) => (q 'or' r)) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
r is Element of CQC-WFF A
(p '&' q) '&' r is Element of CQC-WFF A
q '&' r is Element of CQC-WFF A
p '&' (q '&' r) is Element of CQC-WFF A
((p '&' q) '&' r) => (p '&' (q '&' r)) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' r) 'or' ('not' q) is Element of CQC-WFF A
('not' p) 'or' (('not' r) 'or' ('not' q)) is Element of CQC-WFF A
(('not' r) 'or' ('not' q)) 'or' ('not' p) is Element of CQC-WFF A
(('not' p) 'or' (('not' r) 'or' ('not' q))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) is Element of CQC-WFF A
'not' (q '&' r) is Element of CQC-WFF A
('not' q) 'or' ('not' r) is Element of CQC-WFF A
('not' (q '&' r)) => (('not' q) 'or' ('not' r)) is Element of CQC-WFF A
(('not' q) 'or' ('not' r)) => (('not' r) 'or' ('not' q)) is Element of CQC-WFF A
('not' (q '&' r)) => (('not' r) 'or' ('not' q)) is Element of CQC-WFF A
'not' ('not' p) is Element of CQC-WFF A
('not' ('not' p)) => (('not' (q '&' r)) => (('not' r) 'or' ('not' q))) is Element of CQC-WFF A
('not' ('not' p)) => ('not' (q '&' r)) is Element of CQC-WFF A
('not' ('not' p)) => (('not' r) 'or' ('not' q)) is Element of CQC-WFF A
(('not' ('not' p)) => ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q))) is Element of CQC-WFF A
(('not' ('not' p)) => (('not' (q '&' r)) => (('not' r) 'or' ('not' q)))) => ((('not' ('not' p)) => ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q)))) is Element of CQC-WFF A
('not' p) 'or' ('not' (q '&' r)) is Element of CQC-WFF A
(('not' p) 'or' ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q))) is Element of CQC-WFF A
(('not' p) 'or' ('not' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) is Element of CQC-WFF A
'not' (p '&' (q '&' r)) is Element of CQC-WFF A
('not' (p '&' (q '&' r))) => (('not' p) 'or' ('not' (q '&' r))) is Element of CQC-WFF A
('not' (p '&' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) is Element of CQC-WFF A
('not' (p '&' (q '&' r))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) is Element of CQC-WFF A
'not' (p '&' q) is Element of CQC-WFF A
('not' (p '&' q)) 'or' ('not' r) is Element of CQC-WFF A
'not' ((p '&' q) '&' r) is Element of CQC-WFF A
(('not' (p '&' q)) 'or' ('not' r)) => ('not' ((p '&' q) '&' r)) is Element of CQC-WFF A
('not' q) 'or' ('not' p) is Element of CQC-WFF A
('not' p) 'or' ('not' q) is Element of CQC-WFF A
(('not' q) 'or' ('not' p)) => (('not' p) 'or' ('not' q)) is Element of CQC-WFF A
(('not' p) 'or' ('not' q)) => ('not' (p '&' q)) is Element of CQC-WFF A
(('not' q) 'or' ('not' p)) => ('not' (p '&' q)) is Element of CQC-WFF A
'not' ('not' r) is Element of CQC-WFF A
('not' ('not' r)) => ((('not' q) 'or' ('not' p)) => ('not' (p '&' q))) is Element of CQC-WFF A
('not' ('not' r)) => (('not' q) 'or' ('not' p)) is Element of CQC-WFF A
('not' ('not' r)) => ('not' (p '&' q)) is Element of CQC-WFF A
(('not' ('not' r)) => (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q))) is Element of CQC-WFF A
(('not' ('not' r)) => ((('not' q) 'or' ('not' p)) => ('not' (p '&' q)))) => ((('not' ('not' r)) => (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q)))) is Element of CQC-WFF A
('not' r) 'or' (('not' q) 'or' ('not' p)) is Element of CQC-WFF A
(('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q))) is Element of CQC-WFF A
('not' r) 'or' ('not' (p '&' q)) is Element of CQC-WFF A
(('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' r) 'or' ('not' (p '&' q))) is Element of CQC-WFF A
(('not' r) 'or' ('not' (p '&' q))) => (('not' (p '&' q)) 'or' ('not' r)) is Element of CQC-WFF A
(('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' (p '&' q)) 'or' ('not' r)) is Element of CQC-WFF A
(('not' r) 'or' (('not' q) 'or' ('not' p))) => ('not' ((p '&' q) '&' r)) is Element of CQC-WFF A
((('not' r) 'or' ('not' q)) 'or' ('not' p)) => (('not' r) 'or' (('not' q) 'or' ('not' p))) is Element of CQC-WFF A
('not' (p '&' (q '&' r))) => (('not' r) 'or' (('not' q) 'or' ('not' p))) is Element of CQC-WFF A
('not' (p '&' (q '&' r))) => ('not' ((p '&' q) '&' r)) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
r is Element of CQC-WFF A
q 'or' r is Element of CQC-WFF A
p 'or' (q 'or' r) is Element of CQC-WFF A
(p 'or' q) 'or' r is Element of CQC-WFF A
(p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
('not' r) => q is Element of CQC-WFF A
('not' p) => (('not' r) => q) is Element of CQC-WFF A
('not' p) => q is Element of CQC-WFF A
('not' r) => (('not' p) => q) is Element of CQC-WFF A
(('not' p) => (('not' r) => q)) => (('not' r) => (('not' p) => q)) is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' q) => r is Element of CQC-WFF A
(('not' q) => r) => (('not' r) => q) is Element of CQC-WFF A
('not' p) => ((('not' q) => r) => (('not' r) => q)) is Element of CQC-WFF A
('not' p) => (('not' q) => r) is Element of CQC-WFF A
(('not' p) => (('not' q) => r)) => (('not' p) => (('not' r) => q)) is Element of CQC-WFF A
(('not' p) => ((('not' q) => r) => (('not' r) => q))) => ((('not' p) => (('not' q) => r)) => (('not' p) => (('not' r) => q))) is Element of CQC-WFF A
('not' p) => (q 'or' r) is Element of CQC-WFF A
(p 'or' (q 'or' r)) => (('not' p) => (q 'or' r)) is Element of CQC-WFF A
(p 'or' (q 'or' r)) => (('not' p) => (('not' q) => r)) is Element of CQC-WFF A
(p 'or' (q 'or' r)) => (('not' p) => (('not' r) => q)) is Element of CQC-WFF A
(p 'or' (q 'or' r)) => (('not' r) => (('not' p) => q)) is Element of CQC-WFF A
r 'or' (('not' p) => q) is Element of CQC-WFF A
(p 'or' (q 'or' r)) => (r 'or' (('not' p) => q)) is Element of CQC-WFF A
(('not' p) => q) 'or' r is Element of CQC-WFF A
(r 'or' (('not' p) => q)) => ((('not' p) => q) 'or' r) is Element of CQC-WFF A
(p 'or' (q 'or' r)) => ((('not' p) => q) 'or' r) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
q => (p '&' q) is Element of CQC-WFF A
p => (q => (p '&' q)) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
(p '&' q) 'or' ('not' p) is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
((p '&' q) 'or' ('not' p)) 'or' ('not' q) is Element of CQC-WFF A
('not' q) 'or' ((p '&' q) 'or' ('not' p)) is Element of CQC-WFF A
(((p '&' q) 'or' ('not' p)) 'or' ('not' q)) => (('not' q) 'or' ((p '&' q) 'or' ('not' p))) is Element of CQC-WFF A
'not' (p '&' q) is Element of CQC-WFF A
('not' p) 'or' ('not' q) is Element of CQC-WFF A
('not' (p '&' q)) => (('not' p) 'or' ('not' q)) is Element of CQC-WFF A
(p '&' q) 'or' (('not' p) 'or' ('not' q)) is Element of CQC-WFF A
((p '&' q) 'or' (('not' p) 'or' ('not' q))) => (((p '&' q) 'or' ('not' p)) 'or' ('not' q)) is Element of CQC-WFF A
'not' ('not' q) is Element of CQC-WFF A
('not' ('not' q)) => ((p '&' q) 'or' ('not' p)) is Element of CQC-WFF A
('not' p) 'or' (p '&' q) is Element of CQC-WFF A
((p '&' q) 'or' ('not' p)) => (('not' p) 'or' (p '&' q)) is Element of CQC-WFF A
q => (((p '&' q) 'or' ('not' p)) => (('not' p) 'or' (p '&' q))) is Element of CQC-WFF A
q => ((p '&' q) 'or' ('not' p)) is Element of CQC-WFF A
q => (('not' p) 'or' (p '&' q)) is Element of CQC-WFF A
(q => ((p '&' q) 'or' ('not' p))) => (q => (('not' p) 'or' (p '&' q))) is Element of CQC-WFF A
(q => (((p '&' q) 'or' ('not' p)) => (('not' p) 'or' (p '&' q)))) => ((q => ((p '&' q) 'or' ('not' p))) => (q => (('not' p) 'or' (p '&' q)))) is Element of CQC-WFF A
q => ('not' ('not' q)) is Element of CQC-WFF A
'not' ('not' p) is Element of CQC-WFF A
('not' ('not' p)) => (p '&' q) is Element of CQC-WFF A
q => (('not' ('not' p)) => (p '&' q)) is Element of CQC-WFF A
('not' ('not' p)) => (q => (p '&' q)) is Element of CQC-WFF A
p => ('not' ('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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
q => p is Element of CQC-WFF A
p <=> q is Element of CQC-WFF A
(q => p) => (p <=> q) is Element of CQC-WFF A
(p => q) => ((q => p) => (p <=> q)) is Element of CQC-WFF A
(p => q) '&' (q => p) is Element of CQC-WFF A
(q => p) => ((p => q) '&' (q => p)) is Element of CQC-WFF A
(p => q) => ((q => p) => ((p => q) '&' (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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
q => (p '&' q) is Element of CQC-WFF A
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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
q 'or' p is Element of CQC-WFF A
(p 'or' q) <=> (q 'or' p) is Element of CQC-WFF A
(p 'or' q) => (q 'or' p) is Element of CQC-WFF A
(q 'or' p) => (p 'or' q) is Element of CQC-WFF A
((p 'or' q) => (q 'or' p)) '&' ((q 'or' p) => (p 'or' 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
r is Element of CQC-WFF A
(p '&' q) => r is Element of CQC-WFF A
q => r is Element of CQC-WFF A
p => (q => r) is Element of CQC-WFF A
((p '&' q) => r) => (p => (q => r)) is Element of CQC-WFF A
q => (p '&' q) is Element of CQC-WFF A
((p '&' q) => r) => (q => r) is Element of CQC-WFF A
(q => (p '&' q)) => (((p '&' q) => r) => (q => r)) is Element of CQC-WFF A
p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r))) is Element of CQC-WFF A
p => (q => (p '&' q)) is Element of CQC-WFF A
p => (((p '&' q) => r) => (q => r)) is Element of CQC-WFF A
(p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r))) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
r is Element of CQC-WFF A
q => r is Element of CQC-WFF A
p => (q => r) is Element of CQC-WFF A
(p '&' q) => r is Element of CQC-WFF A
(p => (q => r)) => ((p '&' q) => r) is Element of CQC-WFF A
p => ((p '&' q) => r) is Element of CQC-WFF A
p => r is Element of CQC-WFF A
(p '&' q) => (p => r) is Element of CQC-WFF A
(p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) is Element of CQC-WFF A
(p '&' q) => p is Element of CQC-WFF A
((p '&' q) => p) => ((p '&' q) => r) is Element of CQC-WFF A
((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) is Element of CQC-WFF A
((p '&' q) => (p => r)) => ((p '&' q) => r) is Element of CQC-WFF A
(p '&' q) => q is Element of CQC-WFF A
(q => r) => ((p '&' q) => r) is Element of CQC-WFF A
((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) is Element of CQC-WFF A
p => ((q => r) => ((p '&' q) => r)) is Element of CQC-WFF A
(p => (q => r)) => (p => ((p '&' q) => r)) is Element of CQC-WFF A
(p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) is Element of CQC-WFF A
(p => (q => r)) => ((p '&' q) => (p => r)) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
p => r is Element of CQC-WFF A
q '&' r is Element of CQC-WFF A
p => (q '&' r) is Element of CQC-WFF A
(p => r) => (p => (q '&' r)) is Element of CQC-WFF A
(p => q) => ((p => r) => (p => (q '&' r))) is Element of CQC-WFF A
r => (q '&' r) is Element of CQC-WFF A
q => (r => (q '&' r)) is Element of CQC-WFF A
p => (q => (r => (q '&' r))) is Element of CQC-WFF A
p => (r => (q '&' r)) is Element of CQC-WFF A
(p => q) => (p => (r => (q '&' r))) is Element of CQC-WFF A
(p => (q => (r => (q '&' r)))) => ((p => q) => (p => (r => (q '&' r)))) is Element of CQC-WFF A
(p => (r => (q '&' r))) => ((p => r) => (p => (q '&' r))) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
r is Element of CQC-WFF A
(p 'or' q) => r is Element of CQC-WFF A
p => r is Element of CQC-WFF A
q => r is Element of CQC-WFF A
(p => r) 'or' (q => r) is Element of CQC-WFF A
((p 'or' q) => r) => ((p => r) 'or' (q => r)) is Element of CQC-WFF A
q => (p 'or' q) is Element of CQC-WFF A
((p 'or' q) => r) => (q => r) is Element of CQC-WFF A
(q => (p 'or' q)) => (((p 'or' q) => r) => (q => r)) is Element of CQC-WFF A
'not' (p => r) is Element of CQC-WFF A
('not' (p => r)) => (((p 'or' q) => r) => (q => r)) is Element of CQC-WFF A
('not' (p => r)) => (q => r) is Element of CQC-WFF A
((p 'or' q) => r) => (('not' (p => r)) => (q => r)) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
r => q is Element of CQC-WFF A
p 'or' r is Element of CQC-WFF A
(p 'or' r) => q is Element of CQC-WFF A
(r => q) => ((p 'or' r) => q) is Element of CQC-WFF A
(p => q) => ((r => q) => ((p 'or' r) => 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
'not' r is Element of CQC-WFF A
('not' q) => ('not' r) is Element of CQC-WFF A
('not' p) '&' ('not' r) is Element of CQC-WFF A
('not' q) => (('not' p) '&' ('not' r)) is Element of CQC-WFF A
(('not' q) => ('not' r)) => (('not' q) => (('not' p) '&' ('not' r))) is Element of CQC-WFF A
(('not' q) => ('not' p)) => ((('not' q) => ('not' r)) => (('not' q) => (('not' p) '&' ('not' r)))) is Element of CQC-WFF A
'not' (('not' p) '&' ('not' r)) is Element of CQC-WFF A
('not' (('not' p) '&' ('not' r))) => q is Element of CQC-WFF A
(('not' q) => (('not' p) '&' ('not' r))) => (('not' (('not' p) '&' ('not' r))) => q) is Element of CQC-WFF A
(('not' q) => (('not' p) '&' ('not' r))) => ((p 'or' r) => q) is Element of CQC-WFF A
(('not' q) => ('not' r)) => ((('not' q) => (('not' p) '&' ('not' r))) => ((p 'or' r) => q)) is Element of CQC-WFF A
(('not' q) => ('not' r)) => ((p 'or' r) => q) is Element of CQC-WFF A
((('not' q) => ('not' r)) => (('not' q) => (('not' p) '&' ('not' r)))) => ((('not' q) => ('not' r)) => ((p 'or' r) => q)) is Element of CQC-WFF A
((('not' q) => ('not' r)) => ((('not' q) => (('not' p) '&' ('not' r))) => ((p 'or' r) => q))) => (((('not' q) => ('not' r)) => (('not' q) => (('not' p) '&' ('not' r)))) => ((('not' q) => ('not' r)) => ((p 'or' r) => q))) is Element of CQC-WFF A
(('not' q) => ('not' p)) => ((('not' q) => ('not' r)) => ((p 'or' r) => q)) is Element of CQC-WFF A
(('not' q) => ('not' p)) => ((p 'or' r) => q) is Element of CQC-WFF A
(('not' q) => ('not' r)) => ((('not' q) => ('not' p)) => ((p 'or' r) => q)) is Element of CQC-WFF A
(r => q) => (('not' q) => ('not' r)) is Element of CQC-WFF A
(r => q) => ((('not' q) => ('not' p)) => ((p 'or' r) => q)) is Element of CQC-WFF A
(('not' q) => ('not' p)) => ((r => q) => ((p 'or' r) => q)) is Element of CQC-WFF A
(p => q) => (('not' 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
r => q is Element of CQC-WFF A
(p => q) '&' (r => q) is Element of CQC-WFF A
p 'or' r is Element of CQC-WFF A
(p 'or' r) => q is Element of CQC-WFF A
((p => q) '&' (r => q)) => ((p 'or' r) => q) is Element of CQC-WFF A
(r => q) => ((p 'or' r) => q) is Element of CQC-WFF A
(p => q) => ((r => q) => ((p 'or' r) => q)) is Element of CQC-WFF A
((p => q) => ((r => q) => ((p 'or' r) => q))) => (((p => q) '&' (r => q)) => ((p 'or' r) => 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
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
q '&' ('not' q) is Element of CQC-WFF A
p => (q '&' ('not' q)) is Element of CQC-WFF A
(p => (q '&' ('not' q))) => ('not' p) is Element of CQC-WFF A
'not' (q '&' ('not' q)) is Element of CQC-WFF A
p => ('not' (q '&' ('not' q))) is Element of CQC-WFF A
'not' ('not' (q '&' ('not' q))) is Element of CQC-WFF A
('not' ('not' (q '&' ('not' q)))) => ('not' p) is Element of CQC-WFF A
(q '&' ('not' q)) => ('not' ('not' (q '&' ('not' q)))) is Element of CQC-WFF A
(q '&' ('not' q)) => ('not' p) is Element of CQC-WFF A
p => ((q '&' ('not' q)) => ('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
p => ('not' p) is Element of CQC-WFF A
('not' ('not' p)) => ('not' p) is Element of CQC-WFF A
(p => ('not' p)) => (('not' ('not' p)) => ('not' p)) is Element of CQC-WFF A
(('not' ('not' p)) => p) => ((p => ('not' p)) => (('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' p) is Element of CQC-WFF A
(p => (q '&' ('not' q))) => (p => ('not' p)) is Element of CQC-WFF A
(p => ((q '&' ('not' q)) => ('not' p))) => ((p => (q '&' ('not' q))) => (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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
r is Element of CQC-WFF A
p 'or' r is Element of CQC-WFF A
(p 'or' q) '&' (p 'or' r) is Element of CQC-WFF A
q '&' r is Element of CQC-WFF A
p 'or' (q '&' r) is Element of CQC-WFF A
((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) 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) => r is Element of CQC-WFF A
('not' p) => (q '&' r) is Element of CQC-WFF A
(('not' p) => r) => (('not' p) => (q '&' r)) is Element of CQC-WFF A
(('not' p) => q) => ((('not' p) => r) => (('not' p) => (q '&' r))) is Element of CQC-WFF A
(p 'or' q) => ((('not' p) => r) => (('not' p) => (q '&' r))) is Element of CQC-WFF A
(p 'or' r) => (('not' p) => (q '&' r)) is Element of CQC-WFF A
(p 'or' q) => ((p 'or' r) => (('not' p) => (q '&' r))) is Element of CQC-WFF A
(p 'or' r) => (p 'or' (q '&' r)) is Element of CQC-WFF A
(p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r))) is Element of CQC-WFF A
((p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r)))) => (((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r))) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
r is Element of CQC-WFF A
q 'or' r is Element of CQC-WFF A
p '&' (q 'or' r) is Element of CQC-WFF A
p '&' r is Element of CQC-WFF A
(p '&' q) 'or' (p '&' r) is Element of CQC-WFF A
(p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) is Element of CQC-WFF A
'not' ((p '&' q) 'or' (p '&' r)) is Element of CQC-WFF A
'not' (p '&' q) is Element of CQC-WFF A
'not' (p '&' r) is Element of CQC-WFF A
('not' (p '&' q)) '&' ('not' (p '&' r)) is Element of CQC-WFF A
('not' ((p '&' q) 'or' (p '&' r))) => (('not' (p '&' q)) '&' ('not' (p '&' r))) 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 => ('not' q)) is Element of CQC-WFF A
('not' (p => ('not' q))) => (p '&' q) is Element of CQC-WFF A
('not' (p '&' q)) => (p => ('not' q)) is Element of CQC-WFF A
(('not' (p => ('not' q))) => (p '&' q)) => (('not' (p '&' q)) => (p => ('not' q))) is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
p => ('not' r) is Element of CQC-WFF A
'not' (p => ('not' r)) is Element of CQC-WFF A
('not' (p => ('not' r))) => (p '&' r) is Element of CQC-WFF A
('not' (p '&' r)) => (p => ('not' r)) is Element of CQC-WFF A
(('not' (p => ('not' r))) => (p '&' r)) => (('not' (p '&' r)) => (p => ('not' r))) is Element of CQC-WFF A
('not' q) '&' ('not' r) is Element of CQC-WFF A
p => (('not' q) '&' ('not' r)) is Element of CQC-WFF A
(p => ('not' r)) => (p => (('not' q) '&' ('not' r))) is Element of CQC-WFF A
(p => ('not' q)) => ((p => ('not' r)) => (p => (('not' q) '&' ('not' r)))) is Element of CQC-WFF A
'not' (('not' q) '&' ('not' r)) is Element of CQC-WFF A
p '&' ('not' (('not' q) '&' ('not' r))) is Element of CQC-WFF A
'not' (p '&' ('not' (('not' q) '&' ('not' r)))) is Element of CQC-WFF A
'not' (p '&' (q 'or' r)) is Element of CQC-WFF A
(p => ('not' r)) => ('not' (p '&' (q 'or' r))) is Element of CQC-WFF A
(p => ('not' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) is Element of CQC-WFF A
('not' (p '&' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) is Element of CQC-WFF A
('not' (p '&' q)) => ('not' (p '&' (q 'or' r))) is Element of CQC-WFF A
(p => ('not' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) is Element of CQC-WFF A
('not' (p '&' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) is Element of CQC-WFF A
('not' (p '&' r)) => ('not' (p '&' (q 'or' r))) is Element of CQC-WFF A
('not' (p '&' q)) => (('not' (p '&' r)) => ('not' (p '&' (q 'or' r)))) is Element of CQC-WFF A
(('not' (p '&' q)) '&' ('not' (p '&' r))) => ('not' (p '&' (q 'or' r))) is Element of CQC-WFF A
(('not' (p '&' q)) => (('not' (p '&' r)) => ('not' (p '&' (q 'or' r))))) => ((('not' (p '&' q)) '&' ('not' (p '&' r))) => ('not' (p '&' (q 'or' r)))) is Element of CQC-WFF A
('not' ((p '&' q) 'or' (p '&' r))) => ('not' (p '&' (q 'or' r))) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
r is Element of CQC-WFF A
r 'or' q is Element of CQC-WFF A
(p 'or' q) '&' (r 'or' q) is Element of CQC-WFF A
p '&' r is Element of CQC-WFF A
(p '&' r) 'or' q is Element of CQC-WFF A
((p 'or' q) '&' (r 'or' q)) => ((p '&' r) 'or' q) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
('not' p) => q is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
('not' r) => q is Element of CQC-WFF A
(('not' p) => q) '&' (('not' r) => q) is Element of CQC-WFF A
('not' p) 'or' ('not' r) is Element of CQC-WFF A
(('not' p) 'or' ('not' r)) => q is Element of CQC-WFF A
((('not' p) => q) '&' (('not' r) => q)) => ((('not' p) 'or' ('not' r)) => q) is Element of CQC-WFF A
(p 'or' q) '&' (('not' r) => q) is Element of CQC-WFF A
((p 'or' q) '&' (('not' r) => q)) => ((('not' p) 'or' ('not' r)) => q) is Element of CQC-WFF A
((p 'or' q) '&' (r 'or' q)) => ((('not' p) 'or' ('not' r)) => q) is Element of CQC-WFF A
'not' (p '&' r) is Element of CQC-WFF A
('not' (p '&' r)) => (('not' p) 'or' ('not' r)) is Element of CQC-WFF A
('not' (p '&' r)) => q is Element of CQC-WFF A
((('not' p) 'or' ('not' r)) => q) => (('not' (p '&' r)) => q) is Element of CQC-WFF A
(('not' (p '&' r)) => (('not' p) 'or' ('not' r))) => (((('not' p) 'or' ('not' r)) => q) => (('not' (p '&' r)) => q)) is Element of CQC-WFF A
((p 'or' q) '&' (r 'or' q)) => (('not' (p '&' r)) => 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
r '&' p is Element of CQC-WFF A
r '&' q is Element of CQC-WFF A
(r '&' p) => (r '&' q) is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
r => ('not' q) is Element of CQC-WFF A
'not' (r => ('not' q)) is Element of CQC-WFF A
('not' (r => ('not' q))) => (r '&' 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
r => (('not' q) => ('not' p)) is Element of CQC-WFF A
r => ('not' p) is Element of CQC-WFF A
(r => ('not' q)) => (r => ('not' p)) is Element of CQC-WFF A
(r => (('not' q) => ('not' p))) => ((r => ('not' q)) => (r => ('not' p))) is Element of CQC-WFF A
'not' (r => ('not' p)) is Element of CQC-WFF A
('not' (r => ('not' p))) => ('not' (r => ('not' q))) is Element of CQC-WFF A
(r '&' p) => ('not' (r => ('not' p))) is Element of CQC-WFF A
(r '&' p) => ('not' (r => ('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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
p 'or' r is Element of CQC-WFF A
q 'or' r is Element of CQC-WFF A
(p 'or' r) => (q 'or' r) 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
('not' p) => r is Element of CQC-WFF A
('not' q) => r is Element of CQC-WFF A
(('not' p) => r) => (('not' q) => r) is Element of CQC-WFF A
(('not' q) => ('not' p)) => ((('not' p) => r) => (('not' q) => r)) is Element of CQC-WFF A
(p 'or' r) => (('not' q) => r) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
r 'or' p is Element of CQC-WFF A
r 'or' q is Element of CQC-WFF A
(r 'or' p) => (r 'or' q) is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
('not' r) => (p => q) is Element of CQC-WFF A
('not' r) => p is Element of CQC-WFF A
('not' r) => q is Element of CQC-WFF A
(('not' r) => p) => (('not' r) => q) is Element of CQC-WFF A
(('not' r) => (p => q)) => ((('not' r) => p) => (('not' r) => q)) is Element of CQC-WFF A
(r 'or' p) => (('not' r) => 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
r is Element of CQC-WFF A
(p 'or' q) '&' r is Element of CQC-WFF A
p '&' r is Element of CQC-WFF A
q '&' r is Element of CQC-WFF A
(p '&' r) 'or' (q '&' r) is Element of CQC-WFF A
((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
('not' p) 'or' ('not' r) is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' q) 'or' ('not' r) is Element of CQC-WFF A
(('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)) is Element of CQC-WFF A
'not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r))) is Element of CQC-WFF A
'not' (('not' p) 'or' ('not' r)) is Element of CQC-WFF A
'not' (('not' q) 'or' ('not' r)) is Element of CQC-WFF A
('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r))) is Element of CQC-WFF A
('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) => (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) is Element of CQC-WFF A
('not' p) '&' ('not' q) is Element of CQC-WFF A
(('not' p) '&' ('not' q)) 'or' ('not' r) is Element of CQC-WFF A
((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r))) => ((('not' p) '&' ('not' q)) 'or' ('not' r)) is Element of CQC-WFF A
'not' ((('not' p) '&' ('not' q)) 'or' ('not' r)) is Element of CQC-WFF A
('not' ((('not' p) '&' ('not' q)) 'or' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) is Element of CQC-WFF A
'not' (('not' p) '&' ('not' q)) is Element of CQC-WFF A
'not' ('not' r) is Element of CQC-WFF A
('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r)) is Element of CQC-WFF A
(('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) '&' ('not' q)) 'or' ('not' r))) is Element of CQC-WFF A
(('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) is Element of CQC-WFF A
(p 'or' q) '&' ('not' ('not' r)) is Element of CQC-WFF A
((p 'or' q) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) is Element of CQC-WFF A
'not' (p '&' r) is Element of CQC-WFF A
('not' (p '&' r)) => (('not' p) 'or' ('not' r)) is Element of CQC-WFF A
('not' (('not' p) 'or' ('not' r))) => (p '&' r) is Element of CQC-WFF A
(('not' (p '&' r)) => (('not' p) 'or' ('not' r))) => (('not' (('not' p) 'or' ('not' r))) => (p '&' r)) is Element of CQC-WFF A
(p '&' r) 'or' ('not' (('not' q) 'or' ('not' r))) is Element of CQC-WFF A
(('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) is Element of CQC-WFF A
'not' (q '&' r) is Element of CQC-WFF A
('not' (q '&' r)) => (('not' q) 'or' ('not' r)) is Element of CQC-WFF A
('not' (('not' q) 'or' ('not' r))) => (q '&' r) is Element of CQC-WFF A
(('not' (q '&' r)) => (('not' q) 'or' ('not' r))) => (('not' (('not' q) 'or' ('not' r))) => (q '&' r)) is Element of CQC-WFF A
((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' (q '&' r)) is Element of CQC-WFF A
r => ('not' ('not' r)) is Element of CQC-WFF A
((p 'or' q) '&' r) => ((p 'or' q) '&' ('not' ('not' r))) is Element of CQC-WFF A
((p 'or' q) '&' r) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) is Element of CQC-WFF A
((p 'or' q) '&' r) => (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) is Element of CQC-WFF A
((p 'or' q) '&' r) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
p => (p 'or' 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
q 'or' p is Element of CQC-WFF A
p => (q 'or' 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
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
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
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
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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
(p '&' q) => (p 'or' 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
TAUT A is Element of K6((CQC-WFF A))
K6((CQC-WFF A)) is set
q is Element of CQC-WFF A
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
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
TAUT A is Element of K6((CQC-WFF A))
K6((CQC-WFF A)) is set
r is Element of CQC-WFF A
p 'or' r is Element of CQC-WFF A
q 'or' r is Element of CQC-WFF A
(p 'or' r) => (q 'or' r) 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
TAUT A is Element of K6((CQC-WFF A))
K6((CQC-WFF A)) is set
r is Element of CQC-WFF A
r 'or' p is Element of CQC-WFF A
r 'or' q is Element of CQC-WFF A
(r 'or' p) => (r 'or' 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
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
TAUT A is Element of K6((CQC-WFF A))
K6((CQC-WFF A)) is set
r is Element of CQC-WFF A
r '&' p is Element of CQC-WFF A
r '&' q is Element of CQC-WFF A
(r '&' p) => (r '&' 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
p '&' r is Element of CQC-WFF A
q '&' r is Element of CQC-WFF A
(p '&' r) => (q '&' r) is Element of CQC-WFF A
'not' r is Element of CQC-WFF A
q => ('not' r) is Element of CQC-WFF A
p => ('not' r) is Element of CQC-WFF A
(q => ('not' r)) => (p => ('not' r)) is Element of CQC-WFF A
(p => q) => ((q => ('not' r)) => (p => ('not' r))) is Element of CQC-WFF A
'not' (p => ('not' r)) is Element of CQC-WFF A
'not' (q => ('not' r)) is Element of CQC-WFF A
('not' (p => ('not' r))) => ('not' (q => ('not' r))) is Element of CQC-WFF A
('not' (q => ('not' r))) => (q '&' r) is Element of CQC-WFF A
(p '&' r) => ('not' (p => ('not' r))) is Element of CQC-WFF A
(p '&' r) => ('not' (q => ('not' r))) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
p => r is Element of CQC-WFF A
q '&' r is Element of CQC-WFF A
p => (q '&' r) is Element of CQC-WFF A
(p => r) => (p => (q '&' r)) is Element of CQC-WFF A
(p => q) => ((p => r) => (p => (q '&' r))) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
r => q is Element of CQC-WFF A
p 'or' r is Element of CQC-WFF A
(p 'or' r) => q is Element of CQC-WFF A
(p => q) '&' (r => q) is Element of CQC-WFF A
((p => q) '&' (r => q)) => ((p 'or' r) => 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
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
('not' p) => q is Element of CQC-WFF A
(p 'or' q) => (('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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p 'or' q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
q 'or' p is Element of CQC-WFF A
('not' q) => p is Element of CQC-WFF A
(q 'or' p) => (('not' q) => p) is Element of CQC-WFF A
(p 'or' q) => (q 'or' p) is Element of CQC-WFF A
(p 'or' 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
TAUT A is Element of K6((CQC-WFF A))
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
r is Element of CQC-WFF A
p '&' r is Element of CQC-WFF A
s is Element of CQC-WFF A
r => s is Element of CQC-WFF A
q '&' s is Element of CQC-WFF A
(p '&' r) => (q '&' s) is Element of CQC-WFF A
q '&' r is Element of CQC-WFF A
(p '&' r) => (q '&' r) is Element of CQC-WFF A
(q '&' r) => (q '&' s) 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
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
r is Element of CQC-WFF A
p 'or' r is Element of CQC-WFF A
s is Element of CQC-WFF A
r => s is Element of CQC-WFF A
q 'or' s is Element of CQC-WFF A
(p 'or' r) => (q 'or' s) is Element of CQC-WFF A
q 'or' r is Element of CQC-WFF A
(p 'or' r) => (q 'or' r) is Element of CQC-WFF A
(q 'or' r) => (q 'or' s) 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
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
(p '&' ('not' q)) => ('not' p) is Element of CQC-WFF A
p => q is Element of CQC-WFF A
'not' (p '&' ('not' q)) is Element of CQC-WFF A
'not' ('not' p) is Element of CQC-WFF A
('not' ('not' p)) => ('not' (p '&' ('not' q))) is Element of CQC-WFF A
p => ('not' ('not' p)) is Element of CQC-WFF A
p => ('not' (p '&' ('not' q))) is Element of CQC-WFF A