:: Propositional Calculus
:: by Grzegorz Bancerek, Agata Darmochwa\l and Andrzej Trybulec
::
:: Received September 26, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem Th1: :: LUKASI_1:1

for p, q, r being Element of CQC-WFF holds (p => q) => ((q => r) => (p => r)) in TAUT

proof end;

theorem Th2: :: LUKASI_1:2

for p, q, r being Element of CQC-WFF st p => q in TAUT holds
(q => r) => (p => r) in TAUT

proof end;

theorem Th3: :: LUKASI_1:3

for p, q, r being Element of CQC-WFF st p => q in TAUT & q => r in TAUT holds
p => r in TAUT

proof end;

theorem Th4: :: LUKASI_1:4

for p being Element of CQC-WFF holds p => p in TAUT

proof end;

Lm1: for q, r, p, s being Element of CQC-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT

proof end;

Lm2: for p, q, r, s being Element of CQC-WFF holds (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT

proof end;

Lm3: for p, q, r, s being Element of CQC-WFF holds (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT

proof end;

Lm4: for t, p, r, s, q being Element of CQC-WFF holds (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT

proof end;

Lm5: for p, q, r being Element of CQC-WFF holds ((('not' p) => q) => r) => (p => r) in TAUT

proof end;

Lm6: for p, r, s, q being Element of CQC-WFF holds p => (((('not' p) => r) => s) => ((q => r) => s)) in TAUT

proof end;

Lm7: for q, p being Element of CQC-WFF holds (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT

proof end;

Lm8: for t, p being Element of CQC-WFF holds t => ((('not' p) => p) => p) in TAUT

proof end;

Lm9: for p, q, t being Element of CQC-WFF holds (('not' p) => q) => (t => ((q => p) => p)) in TAUT

proof end;

Lm10: for t, q, p, r being Element of CQC-WFF holds ((t => ((q => p) => p)) => r) => ((('not' p) => q) => r) in TAUT

proof end;

Lm11: for p, q being Element of CQC-WFF holds (('not' p) => q) => ((q => p) => p) in TAUT

proof end;

Lm12: for p, q being Element of CQC-WFF holds p => ((q => p) => p) in TAUT

proof end;

theorem Th5: :: LUKASI_1:5

for q, p being Element of CQC-WFF holds q => (p => q) in TAUT

proof end;

theorem Th6: :: LUKASI_1:6

for p, q, r being Element of CQC-WFF holds ((p => q) => r) => (q => r) in TAUT

proof end;

theorem Th7: :: LUKASI_1:7

for q, p being Element of CQC-WFF holds q => ((q => p) => p) in TAUT

proof end;

theorem Th8: :: LUKASI_1:8

for s, q, p being Element of CQC-WFF holds (s => (q => p)) => (q => (s => p)) in TAUT

proof end;

theorem Th9: :: LUKASI_1:9

for q, r, p being Element of CQC-WFF holds (q => r) => ((p => q) => (p => r)) in TAUT

proof end;

Lm13: for q, s, p, r being Element of CQC-WFF holds ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT

proof end;

Lm14: for p, q being Element of CQC-WFF holds ((p => q) => p) => p in TAUT

proof end;

Lm15: for p, r, s, q being Element of CQC-WFF holds ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT

proof end;

Lm16: for p, q, r being Element of CQC-WFF holds ((p => q) => r) => ((r => p) => p) in TAUT

proof end;

Lm17: for r, p, s, q being Element of CQC-WFF holds (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT

proof end;

Lm18: for q, r, p being Element of CQC-WFF holds ((q => r) => p) => ((q => p) => p) in TAUT

proof end;

theorem Th10: :: LUKASI_1:10

for q, r being Element of CQC-WFF holds (q => (q => r)) => (q => r) in TAUT

proof end;

Lm19: for q, s, r, p being Element of CQC-WFF holds (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT

proof end;

Lm20: for q, r, p, s being Element of CQC-WFF holds ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT

proof end;

Lm21: for q, s, p, r being Element of CQC-WFF holds (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT

proof end;

Lm22: for s, p, q, r being Element of CQC-WFF holds (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT

proof end;

theorem Th11: :: LUKASI_1:11

for p, q, r being Element of CQC-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in TAUT

proof end;

theorem Th12: :: LUKASI_1:12

for p being Element of CQC-WFF holds ('not' VERUM) => p in TAUT

proof end;

theorem Th13: :: LUKASI_1:13

for q, p being Element of CQC-WFF st q in TAUT holds
p => q in TAUT

proof end;

theorem :: LUKASI_1:14

for p, q being Element of CQC-WFF st p in TAUT holds
(p => q) => q in TAUT

proof end;

theorem Th15: :: LUKASI_1:15

for s, q, p being Element of CQC-WFF st s => (q => p) in TAUT holds
q => (s => p) in TAUT

proof end;

theorem Th16: :: LUKASI_1:16

for s, q, p being Element of CQC-WFF st s => (q => p) in TAUT & q in TAUT holds
s => p in TAUT

proof end;

theorem :: LUKASI_1:17

for s, q, p being Element of CQC-WFF st s => (q => p) in TAUT & q in TAUT & s in TAUT holds
p in TAUT

proof end;

theorem :: LUKASI_1:18

for q, r being Element of CQC-WFF st q => (q => r) in TAUT holds
q => r in TAUT

proof end;

theorem Th19: :: LUKASI_1:19

for p, q, r being Element of CQC-WFF st p => (q => r) in TAUT holds
(p => q) => (p => r) in TAUT

proof end;

theorem Th20: :: LUKASI_1:20

for p, q, r being Element of CQC-WFF st p => (q => r) in TAUT & p => q in TAUT holds
p => r in TAUT

proof end;

theorem :: LUKASI_1:21

for p, q, r being Element of CQC-WFF st p => (q => r) in TAUT & p => q in TAUT & p in TAUT holds
r in TAUT

proof end;

theorem Th22: :: LUKASI_1:22

for p, q, r, s being Element of CQC-WFF st p => (q => r) in TAUT & p => (r => s) in TAUT holds
p => (q => s) in TAUT

proof end;

theorem :: LUKASI_1:23

for p being Element of CQC-WFF holds p => VERUM in TAUT by Th13, CQC_THE1:77;

Lm23: for p being Element of CQC-WFF holds ('not' p) => (p => ('not' VERUM)) in TAUT

proof end;

Lm24: for p being Element of CQC-WFF holds (('not' p) => ('not' VERUM)) => p in TAUT

proof end;

theorem Th24: :: LUKASI_1:24

for p, q being Element of CQC-WFF holds (('not' p) => ('not' q)) => (q => p) in TAUT

proof end;

theorem Th25: :: LUKASI_1:25

for p being Element of CQC-WFF holds ('not' ('not' p)) => p in TAUT

proof end;

Lm25: now

let p be Element of CQC-WFF ; :: thesis: (p => ('not' VERUM)) => ('not' p) in TAUT
('not' ('not' p)) => p in TAUT by Th25;
then A1: (p => ('not' VERUM)) => (('not' ('not' p)) => ('not' VERUM)) in TAUT by Th2;
(('not' ('not' p)) => ('not' VERUM)) => ('not' p) in TAUT by Lm24;
hence (p => ('not' VERUM)) => ('not' p) in TAUT by A1, Th3; :: thesis: verum

end;

theorem Th26: :: LUKASI_1:26

for p, q being Element of CQC-WFF holds (p => q) => (('not' q) => ('not' p)) in TAUT

proof end;

theorem Th27: :: LUKASI_1:27

for p being Element of CQC-WFF holds p => ('not' ('not' p)) in TAUT

proof end;

theorem Th28: :: LUKASI_1:28

for p, q being Element of CQC-WFF holds
( (('not' ('not' p)) => q) => (p => q) in TAUT & (p => q) => (('not' ('not' p)) => q) in TAUT )

proof end;

theorem Th29: :: LUKASI_1:29

for p, q being Element of CQC-WFF holds
( (p => ('not' ('not' q))) => (p => q) in TAUT & (p => q) => (p => ('not' ('not' q))) in TAUT )

proof end;

theorem Th30: :: LUKASI_1:30

for p, q being Element of CQC-WFF holds (p => ('not' q)) => (q => ('not' p)) in TAUT

proof end;

theorem Th31: :: LUKASI_1:31

for p, q being Element of CQC-WFF holds (('not' p) => q) => (('not' q) => p) in TAUT

proof end;

theorem :: LUKASI_1:32

for p being Element of CQC-WFF holds (p => ('not' p)) => ('not' p) in TAUT

proof end;

theorem :: LUKASI_1:33

for p, q being Element of CQC-WFF holds ('not' p) => (p => q) in TAUT

proof end;

theorem Th34: :: LUKASI_1:34

for p, q being Element of CQC-WFF holds
( p => q in TAUT iff ('not' q) => ('not' p) in TAUT )

proof end;

theorem :: LUKASI_1:35

for p, q being Element of CQC-WFF st ('not' p) => ('not' q) in TAUT holds
q => p in TAUT by Th34;

theorem :: LUKASI_1:36

for p being Element of CQC-WFF holds
( p in TAUT iff 'not' ('not' p) in TAUT )

proof end;

theorem :: LUKASI_1:37

for p, q being Element of CQC-WFF holds
( p => q in TAUT iff p => ('not' ('not' q)) in TAUT )

proof end;

theorem :: LUKASI_1:38

for p, q being Element of CQC-WFF holds
( p => q in TAUT iff ('not' ('not' p)) => q in TAUT )

proof end;

theorem :: LUKASI_1:39

for p, q being Element of CQC-WFF st p => ('not' q) in TAUT holds
q => ('not' p) in TAUT

proof end;

theorem :: LUKASI_1:40

for p, q being Element of CQC-WFF st ('not' p) => q in TAUT holds
('not' q) => p in TAUT

proof end;

theorem :: LUKASI_1:41

canceled;

registration

let p, q, r be Element of CQC-WFF ;
cluster K154((p => q),((q => r) => (p => r))) -> valid ;
coherence
(p => q) => ((q => r) => (p => r)) is valid

proof end;

end;

theorem :: LUKASI_1:42

for p, q, r being Element of CQC-WFF st p => q is valid holds
(q => r) => (p => r) is valid

proof end;

theorem Th43: :: LUKASI_1:43

for p, q, r being Element of CQC-WFF st p => q is valid & q => r is valid holds
p => r is valid

proof end;

theorem :: LUKASI_1:44

canceled;

theorem :: LUKASI_1:45

canceled;

registration

let p be Element of CQC-WFF ;
cluster K154(p,p) -> valid ;
coherence
p => p is valid

proof end;

end;

registration

let p, q be Element of CQC-WFF ;
cluster K154(p,(q => p)) -> valid ;
coherence
p => (q => p) is valid

proof end;

end;

theorem :: LUKASI_1:46

for p, q being Element of CQC-WFF st p is valid holds
q => p is valid

proof end;

theorem :: LUKASI_1:47

canceled;

registration

let p, q, s be Element of CQC-WFF ;
cluster K154((s => (q => p)),(q => (s => p))) -> valid ;
coherence
(s => (q => p)) => (q => (s => p)) is valid

proof end;

end;

theorem Th48: :: LUKASI_1:48

for p, q, r being Element of CQC-WFF st p => (q => r) is valid holds
q => (p => r) is valid

proof end;

theorem :: LUKASI_1:49

for p, q, r being Element of CQC-WFF st p => (q => r) is valid & q is valid holds
p => r is valid

proof end;

theorem :: LUKASI_1:50

for p being Element of CQC-WFF holds
( p => VERUM is valid & ('not' VERUM) => p is valid )

proof end;

theorem :: LUKASI_1:51

canceled;

theorem :: LUKASI_1:52

canceled;

registration

let p, q be Element of CQC-WFF ;
cluster K154(p,((p => q) => q)) -> valid ;
coherence
p => ((p => q) => q) is valid

proof end;

end;

registration

let q, r be Element of CQC-WFF ;
cluster K154((q => (q => r)),(q => r)) -> valid ;
coherence
(q => (q => r)) => (q => r) is valid

proof end;

end;

theorem :: LUKASI_1:53

for q, r being Element of CQC-WFF st q => (q => r) is valid holds
q => r is valid

proof end;

theorem :: LUKASI_1:54

canceled;

registration

let p, q, r be Element of CQC-WFF ;
cluster K154((p => (q => r)),((p => q) => (p => r))) -> valid ;
coherence
(p => (q => r)) => ((p => q) => (p => r)) is valid

proof end;

end;

theorem Th55: :: LUKASI_1:55

for p, q, r being Element of CQC-WFF st p => (q => r) is valid holds
(p => q) => (p => r) is valid

proof end;

theorem :: LUKASI_1:56

for p, q, r being Element of CQC-WFF st p => (q => r) is valid & p => q is valid holds
p => r is valid

proof end;

theorem :: LUKASI_1:57

canceled;

registration

let p, q, r be Element of CQC-WFF ;
cluster K154(((p => q) => r),(q => r)) -> valid ;
coherence
((p => q) => r) => (q => r) is valid

proof end;

end;

theorem :: LUKASI_1:58

for p, q, r being Element of CQC-WFF st (p => q) => r is valid holds
q => r is valid

proof end;

theorem :: LUKASI_1:59

canceled;

registration

let p, q, r be Element of CQC-WFF ;
cluster K154((p => q),((r => p) => (r => q))) -> valid ;
coherence
(p => q) => ((r => p) => (r => q)) is valid

proof end;

end;

theorem :: LUKASI_1:60

for p, q, r being Element of CQC-WFF st p => q is valid holds
(r => p) => (r => q) is valid

proof end;

theorem :: LUKASI_1:61

canceled;

theorem :: LUKASI_1:62

canceled;

registration

let p, q be Element of CQC-WFF ;
cluster K154((p => q),(('not' q) => ('not' p))) -> valid ;
coherence
(p => q) => (('not' q) => ('not' p)) is valid

proof end;

end;

registration

let p, q be Element of CQC-WFF ;
cluster K154((('not' p) => ('not' q)),(q => p)) -> valid ;
coherence
(('not' p) => ('not' q)) => (q => p) is valid

proof end;

end;

theorem :: LUKASI_1:63

for p, q being Element of CQC-WFF holds
( ('not' p) => ('not' q) is valid iff q => p is valid )

proof end;

theorem :: LUKASI_1:64

canceled;

theorem :: LUKASI_1:65

canceled;

registration

let p be Element of CQC-WFF ;
cluster K154(p,('not' ('not' p))) -> valid ;
coherence
p => ('not' ('not' p)) is valid

proof end;

end;

registration

let p be Element of CQC-WFF ;
cluster K154(('not' ('not' p)),p) -> valid ;
coherence
('not' ('not' p)) => p is valid

proof end;

end;

theorem :: LUKASI_1:66

for p being Element of CQC-WFF holds
( 'not' ('not' p) is valid iff p is valid )

proof end;

theorem :: LUKASI_1:67

canceled;

registration

let p, q be Element of CQC-WFF ;
cluster K154((('not' ('not' p)) => q),(p => q)) -> valid ;
coherence
(('not' ('not' p)) => q) => (p => q) is valid

proof end;

end;

theorem :: LUKASI_1:68

for p, q being Element of CQC-WFF holds
( ('not' ('not' p)) => q is valid iff p => q is valid )

proof end;

theorem :: LUKASI_1:69

canceled;

registration

let p, q be Element of CQC-WFF ;
cluster K154((p => ('not' ('not' q))),(p => q)) -> valid ;
coherence
(p => ('not' ('not' q))) => (p => q) is valid

proof end;

end;

theorem :: LUKASI_1:70

for p, q being Element of CQC-WFF holds
( p => ('not' ('not' q)) is valid iff p => q is valid )

proof end;

theorem :: LUKASI_1:71

canceled;

registration

let p, q be Element of CQC-WFF ;
cluster K154((p => ('not' q)),(q => ('not' p))) -> valid ;
coherence
(p => ('not' q)) => (q => ('not' p)) is valid

proof end;

end;

theorem :: LUKASI_1:72

for p, q being Element of CQC-WFF st p => ('not' q) is valid holds
q => ('not' p) is valid

proof end;

theorem :: LUKASI_1:73

canceled;

registration

let p, q be Element of CQC-WFF ;
cluster K154((('not' p) => q),(('not' q) => p)) -> valid ;
coherence
(('not' p) => q) => (('not' q) => p) is valid

proof end;

end;

theorem :: LUKASI_1:74

for p, q being Element of CQC-WFF st ('not' p) => q is valid holds
('not' q) => p is valid

proof end;

theorem :: LUKASI_1:75

for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => q holds
X |- (q => r) => (p => r)

proof end;

theorem Th76: :: LUKASI_1:76

for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => q & X |- q => r holds
X |- p => r

proof end;

theorem :: LUKASI_1:77

for p being Element of CQC-WFF
for X being Subset of CQC-WFF holds X |- p => p by CQC_THE1:98;

theorem :: LUKASI_1:78

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p holds
X |- q => p

proof end;

theorem :: LUKASI_1:79

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p holds
X |- (p => q) => q

proof end;

theorem Th80: :: LUKASI_1:80

for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => (q => r) holds
X |- q => (p => r)

proof end;

theorem :: LUKASI_1:81

for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => (q => r) & X |- q holds
X |- p => r

proof end;

theorem :: LUKASI_1:82

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => (p => q) holds
X |- p => q

proof end;

theorem :: LUKASI_1:83

for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- (p => q) => r holds
X |- q => r

proof end;

theorem Th84: :: LUKASI_1:84

for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => (q => r) holds
X |- (p => q) => (p => r)

proof end;

theorem :: LUKASI_1:85

for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => (q => r) & X |- p => q holds
X |- p => r

proof end;

theorem :: LUKASI_1:86

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds
( X |- ('not' p) => ('not' q) iff X |- q => p )

proof end;

theorem :: LUKASI_1:87

for p being Element of CQC-WFF
for X being Subset of CQC-WFF holds
( X |- 'not' ('not' p) iff X |- p )

proof end;

theorem :: LUKASI_1:88

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds
( X |- p => ('not' ('not' q)) iff X |- p => q )

proof end;

theorem :: LUKASI_1:89

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds
( X |- ('not' ('not' p)) => q iff X |- p => q )

proof end;

theorem Th90: :: LUKASI_1:90

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => ('not' q) holds
X |- q => ('not' p)

proof end;

theorem Th91: :: LUKASI_1:91

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- ('not' p) => q holds
X |- ('not' q) => p

proof end;

theorem :: LUKASI_1:92

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- p => ('not' q) & X |- q holds
X |- 'not' p

proof end;

theorem :: LUKASI_1:93

for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st X |- ('not' p) => q & X |- 'not' q holds
X |- p

proof end;