:: Logical Equivalence of Formulae
:: by Oleg Okhotnikov
::
:: Received January 24, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: CQC_THE3:1
theorem Th2: :: CQC_THE3:2
theorem Th3: :: CQC_THE3:3
theorem Th4: :: CQC_THE3:4
:: deftheorem Def1 defines |- CQC_THE3:def 1 :
theorem Th5: :: CQC_THE3:5
theorem Th6: :: CQC_THE3:6
:: deftheorem Def2 defines |- CQC_THE3:def 2 :
theorem Th7: :: CQC_THE3:7
theorem :: CQC_THE3:8
theorem Th9: :: CQC_THE3:9
theorem Th10: :: CQC_THE3:10
theorem Th11: :: CQC_THE3:11
theorem :: CQC_THE3:12
theorem Th13: :: CQC_THE3:13
theorem Th14: :: CQC_THE3:14
:: deftheorem Def3 defines |- CQC_THE3:def 3 :
theorem Th15: :: CQC_THE3:15
theorem :: CQC_THE3:16
theorem :: CQC_THE3:17
:: deftheorem Def4 defines |-| CQC_THE3:def 4 :
theorem Th18: :: CQC_THE3:18
theorem Th19: :: CQC_THE3:19
theorem Th20: :: CQC_THE3:20
Lm1:
for X, Y being Subset of CQC-WFF holds X \/ Y c= (Cn X) \/ (Cn Y)
theorem Th21: :: CQC_THE3:21
theorem Th22: :: CQC_THE3:22
theorem :: CQC_THE3:23
theorem :: CQC_THE3:24
theorem Th25: :: CQC_THE3:25
theorem Th26: :: CQC_THE3:26
theorem Th27: :: CQC_THE3:27
:: deftheorem Def5 defines |-| CQC_THE3:def 5 :
theorem Th28: :: CQC_THE3:28
theorem Th29: :: CQC_THE3:29
theorem :: CQC_THE3:30
theorem Th31: :: CQC_THE3:31
theorem :: CQC_THE3:32
Lm2:
for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p & X |- q holds
X |- p '&' q
Lm3:
for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p '&' q holds
( X |- p & X |- q )
theorem :: CQC_THE3:33
Lm4:
for p, q, r, s being Element of CQC-WFF st p |-| q & r |-| s holds
p '&' r |- q '&' s
theorem :: CQC_THE3:34
theorem Th35: :: CQC_THE3:35
theorem Th36: :: CQC_THE3:36
theorem :: CQC_THE3:37
:: deftheorem Def6 defines is_an_universal_closure_of CQC_THE3:def 6 :
theorem Th38: :: CQC_THE3:38
theorem Th39: :: CQC_THE3:39
theorem Th40: :: CQC_THE3:40
theorem Th41: :: CQC_THE3:41
theorem :: CQC_THE3:42
theorem Th43: :: CQC_THE3:43
theorem :: CQC_THE3:44
theorem Th45: :: CQC_THE3:45
theorem :: CQC_THE3:46
theorem :: CQC_THE3:47
theorem Th48: :: CQC_THE3:48
theorem :: CQC_THE3:49
:: deftheorem Def7 defines <==> CQC_THE3:def 7 :
theorem Th50: :: CQC_THE3:50
theorem :: CQC_THE3:51
theorem :: CQC_THE3:52
Lm5:
for p, q being Element of CQC-WFF st p <==> q holds
'not' p <==> 'not' q
Lm6:
for p, q being Element of CQC-WFF st 'not' p <==> 'not' q holds
p <==> q
theorem :: CQC_THE3:53
theorem Th54: :: CQC_THE3:54
theorem Th55: :: CQC_THE3:55
theorem :: CQC_THE3:56
theorem :: CQC_THE3:57
theorem Th58: :: CQC_THE3:58
theorem :: CQC_THE3:59
theorem :: CQC_THE3:60
canceled;
theorem Th61: :: CQC_THE3:61
theorem Th62: :: CQC_THE3:62
theorem Th63: :: CQC_THE3:63
theorem Th64: :: CQC_THE3:64
theorem Th65: :: CQC_THE3:65
theorem :: CQC_THE3:66