:: Calculus of Quantifiers. Deduction Theorem
:: by Agata Darmochwa\l
::
:: Received October 24, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: CQC_THE2:1
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(p '&' q) => r is valid
proofend;

theorem Th2: :: CQC_THE2:2
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(q '&' p) => r is valid
proofend;

theorem Th3: :: CQC_THE2:3
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds
p => (q => r) is valid
proofend;

theorem Th4: :: CQC_THE2:4
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds
q => (p => r) is valid
proofend;

Lm1:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )
proofend;

Lm2:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q is valid holds
( p is valid & q is valid )
proofend;

Lm3:  for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & p => r is valid holds
p => (q '&' r) is valid
proofend;

Lm4:  for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p 'or' r) => (q 'or' t) is valid
proofend;

Lm5:  for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p '&' r) => (q '&' t) is valid
proofend;

Lm6:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
proofend;

Lm7:  for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & r => q is valid holds
(p 'or' r) => q is valid
proofend;

Lm8:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is valid & q is valid holds
p '&' q is valid
proofend;

Lm9:  for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r '&' p) => (r '&' q) is valid
proofend;

Lm10:  for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(p 'or' r) => (q 'or' r) is valid
proofend;

Lm11:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid
proofend;

Lm12:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid
proofend;

Lm13:  for A being QC-alphabet
for p being Element of CQC-WFF A holds p <=> p is valid
proofend;

Lm14:  for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ( p => q is valid &amp; q => p is valid ) iff p <=> q is valid )
proofend;

Lm15:  for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <=> q is valid holds
( p is valid iff q is valid )
proofend;

Lm16:  for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid &amp; r => t is valid holds
p => (q => t) is valid
proofend;

::------------------------------------------------
theorem Th5: :: CQC_THE2:5
for A being QC-alphabet
for s being QC-formula of A
for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s &amp; y <> x ) )
proofend;

theorem Th6: :: CQC_THE2:6
for A being QC-alphabet
for s being QC-formula of A
for y, x being bound_QC-variable of A holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s &amp; y <> x ) )
proofend;

theorem Th7: :: CQC_THE2:7
for A being QC-alphabet
for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
proofend;

theorem Th8: :: CQC_THE2:8
for A being QC-alphabet
for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s '&amp;' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
proofend;

theorem Th9: :: CQC_THE2:9
for A being QC-alphabet
for s, h being QC-formula of A
for y being bound_QC-variable of A holds
( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
proofend;

theorem :: CQC_THE2:10
for A being QC-alphabet
for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (All (x,y,s)) &amp; not y in still_not-bound_in (All (x,y,s)) )
proofend;

theorem :: CQC_THE2:11
for A being QC-alphabet
for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (Ex (x,y,s)) &amp; not y in still_not-bound_in (Ex (x,y,s)) )
proofend;

theorem Th12: :: CQC_THE2:12
for A being QC-alphabet
for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s => h) . x = (s . x) => (h . x)
proofend;

theorem :: CQC_THE2:13
for A being QC-alphabet
for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x)
proofend;

theorem :: CQC_THE2:14
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A st x <> y holds
(Ex (x,p)) . y = Ex (x,(p . y))
proofend;

::---------------------------------------------------------
theorem Th15: :: CQC_THE2:15
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid
proofend;

theorem Th16: :: CQC_THE2:16
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st p is valid holds
Ex (x,p) is valid
proofend;

theorem :: CQC_THE2:17
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid
proofend;

theorem :: CQC_THE2:18
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds (All (x,p)) => (Ex (y,p)) is valid
proofend;

theorem Th19: :: CQC_THE2:19
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p => q is valid &amp; not x in still_not-bound_in q holds
(Ex (x,p)) => q is valid
proofend;

theorem Th20: :: CQC_THE2:20
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => p is valid
proofend;

theorem :: CQC_THE2:21
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p &amp; Ex (x,p) is valid holds
p is valid
proofend;

theorem Th22: :: CQC_THE2:22
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; q = h . y &amp; not y in still_not-bound_in h holds
p => (Ex (y,q)) is valid
proofend;

theorem Th23: :: CQC_THE2:23
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st p is valid holds
All (x,p) is valid
proofend;

theorem Th24: :: CQC_THE2:24
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
p => (All (x,p)) is valid
proofend;

theorem Th25: :: CQC_THE2:25
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; q = h . y &amp; not x in still_not-bound_in h holds
(All (x,p)) => q is valid
proofend;

theorem :: CQC_THE2:26
for A being QC-alphabet
for p being Element of CQC-WFF A
for y, x being bound_QC-variable of A st not y in still_not-bound_in p holds
(All (x,p)) => (All (y,p)) is valid
proofend;

theorem :: CQC_THE2:27
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; q = h . y &amp; not x in still_not-bound_in h &amp; not y in still_not-bound_in p holds
(All (x,p)) => (All (y,q)) is valid
proofend;

theorem :: CQC_THE2:28
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,p)) => (Ex (y,p)) is valid
proofend;

theorem :: CQC_THE2:29
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; q = h . y &amp; not x in still_not-bound_in q &amp; not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (y,q)) is valid
proofend;

theorem Th30: :: CQC_THE2:30
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid
proofend;

theorem Th31: :: CQC_THE2:31
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(All (x,p)) => (All (x,q)) is valid
proofend;

theorem Th32: :: CQC_THE2:32
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid
proofend;

theorem :: CQC_THE2:33
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p <=> q)) is valid holds
(All (x,p)) <=> (All (x,q)) is valid
proofend;

theorem Th34: :: CQC_THE2:34
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid
proofend;

theorem Th35: :: CQC_THE2:35
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st All (x,(p => q)) is valid holds
(Ex (x,p)) => (Ex (x,q)) is valid
proofend;

theorem Th36: :: CQC_THE2:36
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (All (x,(p '&amp;' q))) => ((All (x,p)) '&amp;' (All (x,q))) is valid &amp; ((All (x,p)) '&amp;' (All (x,q))) => (All (x,(p '&amp;' q))) is valid )
proofend;

theorem Th37: :: CQC_THE2:37
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&amp;' q))) <=> ((All (x,p)) '&amp;' (All (x,q))) is valid
proofend;

theorem :: CQC_THE2:38
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( All (x,(p '&amp;' q)) is valid iff (All (x,p)) '&amp;' (All (x,q)) is valid )
proofend;

theorem Th39: :: CQC_THE2:39
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid
proofend;

theorem Th40: :: CQC_THE2:40
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid &amp; ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid )
proofend;

theorem Th41: :: CQC_THE2:41
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid
proofend;

theorem :: CQC_THE2:42
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid )
proofend;

theorem Th43: :: CQC_THE2:43
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p '&amp;' q))) => ((Ex (x,p)) '&amp;' (Ex (x,q))) is valid
proofend;

theorem :: CQC_THE2:44
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st Ex (x,(p '&amp;' q)) is valid holds
(Ex (x,p)) '&amp;' (Ex (x,q)) is valid
proofend;

theorem Th45: :: CQC_THE2:45
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (All (x,('not' ('not' p)))) => (All (x,p)) is valid &amp; (All (x,p)) => (All (x,('not' ('not' p)))) is valid )
proofend;

theorem :: CQC_THE2:46
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid
proofend;

theorem Th47: :: CQC_THE2:47
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid &amp; (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid )
proofend;

theorem :: CQC_THE2:48
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid
proofend;

theorem Th49: :: CQC_THE2:49
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid &amp; (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid )
proofend;

theorem :: CQC_THE2:50
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid
proofend;

theorem Th51: :: CQC_THE2:51
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid &amp; (Ex (x,('not' p))) => ('not' (All (x,p))) is valid )
proofend;

theorem :: CQC_THE2:52
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid
proofend;

theorem :: CQC_THE2:53
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid &amp; (All (x,('not' p))) => ('not' (Ex (x,p))) is valid )
proofend;

theorem Th54: :: CQC_THE2:54
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid
proofend;

theorem :: CQC_THE2:55
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid &amp; (All (x,y,p)) => (All (y,x,p)) is valid )
proofend;

theorem :: CQC_THE2:56
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; q = h . y &amp; not y in still_not-bound_in h holds
(All (x,(All (y,q)))) => (All (x,p)) is valid
proofend;

theorem :: CQC_THE2:57
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid &amp; (Ex (x,y,p)) => (Ex (y,x,p)) is valid )
proofend;

theorem :: CQC_THE2:58
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x &amp; q = h . y &amp; not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (x,y,q)) is valid
proofend;

theorem :: CQC_THE2:59
for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid
proofend;

theorem :: CQC_THE2:60
for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds Ex (x,(p <=> p)) is valid by Lm13, Th16;

theorem Th61: :: CQC_THE2:61
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid &amp; ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid )
proofend;

theorem Th62: :: CQC_THE2:62
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid
proofend;

theorem :: CQC_THE2:63
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds
( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid )
proofend;

theorem Th64: :: CQC_THE2:64
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&amp;' q))) => (p '&amp;' (All (x,q))) is valid
proofend;

theorem Th65: :: CQC_THE2:65
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&amp;' q))) => ((All (x,p)) '&amp;' q) is valid
proofend;

theorem Th66: :: CQC_THE2:66
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&amp;' (All (x,q))) => (All (x,(p '&amp;' q))) is valid
proofend;

theorem :: CQC_THE2:67
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p &amp; p '&amp;' (All (x,q)) is valid holds
All (x,(p '&amp;' q)) is valid
proofend;

theorem Th68: :: CQC_THE2:68
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid &amp; (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid )
proofend;

theorem Th69: :: CQC_THE2:69
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid
proofend;

theorem :: CQC_THE2:70
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid )
proofend;

theorem Th71: :: CQC_THE2:71
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p '&amp;' (Ex (x,q))) => (Ex (x,(p '&amp;' q))) is valid &amp; (Ex (x,(p '&amp;' q))) => (p '&amp;' (Ex (x,q))) is valid )
proofend;

theorem Th72: :: CQC_THE2:72
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p '&amp;' (Ex (x,q))) <=> (Ex (x,(p '&amp;' q))) is valid
proofend;

theorem :: CQC_THE2:73
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p '&amp;' (Ex (x,q)) is valid iff Ex (x,(p '&amp;' q)) is valid )
proofend;

Lm17:  for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(All (x,(p => q))) => (p => (All (x,q))) is valid
proofend;

theorem Th74: :: CQC_THE2:74
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (All (x,(p => q))) => (p => (All (x,q))) is valid &amp; (p => (All (x,q))) => (All (x,(p => q))) is valid )
proofend;

theorem Th75: :: CQC_THE2:75
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (All (x,q))) <=> (All (x,(p => q))) is valid
proofend;

theorem :: CQC_THE2:76
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( All (x,(p => q)) is valid iff p => (All (x,q)) is valid )
proofend;

theorem Th77: :: CQC_THE2:77
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
(Ex (x,(p => q))) => ((All (x,p)) => q) is valid
proofend;

theorem Th78: :: CQC_THE2:78
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid
proofend;

theorem :: CQC_THE2:79
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid )
proofend;

theorem Th80: :: CQC_THE2:80
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid &amp; (All (x,(p => q))) => ((Ex (x,p)) => q) is valid )
proofend;

theorem Th81: :: CQC_THE2:81
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid
proofend;

theorem :: CQC_THE2:82
for A being QC-alphabet
for q, p being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in q holds
( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid )
proofend;

theorem Th83: :: CQC_THE2:83
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
proofend;

theorem Th84: :: CQC_THE2:84
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
proofend;

theorem Th85: :: CQC_THE2:85
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid
proofend;

theorem :: CQC_THE2:86
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid )
proofend;

theorem :: CQC_THE2:87
for A being QC-alphabet
for p being Element of CQC-WFF A holds {p} |- p
proofend;

theorem Th88: :: CQC_THE2:88
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds Cn ({p} \/ {q}) = Cn {(p '&amp;' q)}
proofend;

theorem :: CQC_THE2:89
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds
( {p,q} |- r iff {(p '&amp;' q)} |- r )
proofend;

theorem Th90: :: CQC_THE2:90
for A being QC-alphabet
for X being Subset of (CQC-WFF A)
for p being Element of CQC-WFF A
for x being bound_QC-variable of A st X |- p holds
X |- All (x,p)
proofend;

theorem :: CQC_THE2:91
for A being QC-alphabet
for X being Subset of (CQC-WFF A)
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
X |- (All (x,(p => q))) => (p => (All (x,q))) by Th74, CQC_THE1:59;

:: [WP: ] Deduction_Theorem
theorem :: CQC_THE2:92
for A being QC-alphabet
for X being Subset of (CQC-WFF A)
for F, G being Element of CQC-WFF A st F is closed &amp; X \/ {F} |- G holds
X |- F => G
proofend;