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

theorem Th1: :: LUKASI_1:1
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p => q) => ((q => r) => (p => r)) in TAUT A
proof end;

theorem Th2: :: LUKASI_1:2
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(q => r) => (p => r) in TAUT A
proof end;

theorem Th3: :: LUKASI_1:3
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A & q => r in TAUT A holds
p => r in TAUT A
proof end;

theorem Th4: :: LUKASI_1:4
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => p in TAUT A
proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm7: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (q => ((() => p) => p)) => ((() => p) => p) in TAUT A

proof end;

Lm8: for A being QC-alphabet
for p, t being Element of CQC-WFF A holds t => ((() => p) => p) in TAUT A

proof end;

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

proof end;

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

proof end;

Lm11: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (() => q) => ((q => p) => p) in TAUT A

proof end;

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

proof end;

theorem Th5: :: LUKASI_1:5
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds q => (p => q) in TAUT A
proof end;

theorem Th6: :: LUKASI_1:6
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p => q) => r) => (q => r) in TAUT A
proof end;

theorem Th7: :: LUKASI_1:7
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds q => ((q => p) => p) in TAUT A
proof end;

theorem Th8: :: LUKASI_1:8
for A being QC-alphabet
for p, q, s being Element of CQC-WFF A holds (s => (q => p)) => (q => (s => p)) in TAUT A
proof end;

theorem Th9: :: LUKASI_1:9
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (q => r) => ((p => q) => (p => r)) in TAUT A
proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th10: :: LUKASI_1:10
for A being QC-alphabet
for q, r being Element of CQC-WFF A holds (q => (q => r)) => (q => r) in TAUT A
proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th11: :: LUKASI_1:11
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p => q) => (p => r)) in TAUT A
proof end;

theorem Th12: :: LUKASI_1:12
for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' ()) => p in TAUT A
proof end;

theorem Th13: :: LUKASI_1:13
for A being QC-alphabet
for p, q being Element of CQC-WFF A st q in TAUT A holds
p => q in TAUT A
proof end;

theorem :: LUKASI_1:14
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A holds
(p => q) => q in TAUT A
proof end;

theorem Th15: :: LUKASI_1:15
for A being QC-alphabet
for p, q, s being Element of CQC-WFF A st s => (q => p) in TAUT A holds
q => (s => p) in TAUT A
proof end;

theorem Th16: :: LUKASI_1:16
for A being QC-alphabet
for p, q, s being Element of CQC-WFF A st s => (q => p) in TAUT A & q in TAUT A holds
s => p in TAUT A
proof end;

theorem :: LUKASI_1:17
for A being QC-alphabet
for p, q, s being Element of CQC-WFF A st s => (q => p) in TAUT A & q in TAUT A & s in TAUT A holds
p in TAUT A
proof end;

theorem :: LUKASI_1:18
for A being QC-alphabet
for q, r being Element of CQC-WFF A st q => (q => r) in TAUT A holds
q => r in TAUT A
proof end;

theorem Th19: :: LUKASI_1:19
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A holds
(p => q) => (p => r) in TAUT A
proof end;

theorem Th20: :: LUKASI_1:20
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A & p => q in TAUT A holds
p => r in TAUT A
proof end;

theorem :: LUKASI_1:21
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A & p => q in TAUT A & p in TAUT A holds
r in TAUT A
proof end;

theorem Th22: :: LUKASI_1:22
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p => (q => r) in TAUT A & p => (r => s) in TAUT A holds
p => (q => s) in TAUT A
proof end;

theorem :: LUKASI_1:23
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => () in TAUT A by ;

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

proof end;

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

proof end;

theorem Th24: :: LUKASI_1:24
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (() => ()) => (q => p) in TAUT A
proof end;

theorem Th25: :: LUKASI_1:25
for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' ()) => p in TAUT A
proof end;

Lm25: now :: thesis: for A being QC-alphabet
for p being Element of CQC-WFF A holds (p => ('not' ())) => () in TAUT A
let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds (p => ('not' ())) => () in TAUT A
let p be Element of CQC-WFF A; :: thesis: (p => ('not' ())) => () in TAUT A
('not' ()) => p in TAUT A by Th25;
then A1: (p => ('not' ())) => (('not' ()) => ('not' ())) in TAUT A by Th2;
(('not' ()) => ('not' ())) => () in TAUT A by Lm24;
hence (p => ('not' ())) => () in TAUT A by ; :: thesis: verum
end;

theorem Th26: :: LUKASI_1:26
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => q) => (() => ()) in TAUT A
proof end;

theorem Th27: :: LUKASI_1:27
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => ('not' ()) in TAUT A
proof end;

theorem Th28: :: LUKASI_1:28
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (('not' ()) => q) => (p => q) in TAUT A & (p => q) => (('not' ()) => q) in TAUT A )
proof end;

theorem Th29: :: LUKASI_1:29
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (p => ('not' ())) => (p => q) in TAUT A & (p => q) => (p => ('not' ())) in TAUT A )
proof end;

theorem Th30: :: LUKASI_1:30
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => ()) => (q => ()) in TAUT A
proof end;

theorem Th31: :: LUKASI_1:31
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (() => q) => (() => p) in TAUT A
proof end;

theorem :: LUKASI_1:32
for A being QC-alphabet
for p being Element of CQC-WFF A holds (p => ()) => () in TAUT A
proof end;

theorem :: LUKASI_1:33
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds () => (p => q) in TAUT A
proof end;

theorem Th34: :: LUKASI_1:34
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff () => () in TAUT A )
proof end;

theorem :: LUKASI_1:35
for A being QC-alphabet
for p, q being Element of CQC-WFF A st () => () in TAUT A holds
q => p in TAUT A by Th34;

theorem :: LUKASI_1:36
for A being QC-alphabet
for p being Element of CQC-WFF A holds
( p in TAUT A iff 'not' () in TAUT A )
proof end;

theorem :: LUKASI_1:37
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff p => ('not' ()) in TAUT A )
proof end;

theorem :: LUKASI_1:38
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff ('not' ()) => q in TAUT A )
proof end;

theorem :: LUKASI_1:39
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p => () in TAUT A holds
q => () in TAUT A
proof end;

theorem :: LUKASI_1:40
for A being QC-alphabet
for p, q being Element of CQC-WFF A st () => q in TAUT A holds
() => p in TAUT A
proof end;

:: predykat |- i schematy konsekwencji
registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
cluster K166(A,(p => q),((q => r) => (p => r))) -> valid ;
coherence
(p => q) => ((q => r) => (p => r)) is valid
by Th1;
end;

theorem :: LUKASI_1:41
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(q => r) => (p => r) is valid
proof end;

theorem Th42: :: LUKASI_1:42
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & q => r is valid holds
p => r is valid by Th3;

registration
let A be QC-alphabet ;
let p be Element of CQC-WFF A;
cluster K166(A,p,p) -> valid ;
coherence
p => p is valid
by Th4;
end;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,p,(q => p)) -> valid ;
coherence
p => (q => p) is valid
by Th5;
end;

theorem :: LUKASI_1:43
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is valid holds
q => p is valid by Th13;

registration
let A be QC-alphabet ;
let p, q, s be Element of CQC-WFF A;
cluster K166(A,(s => (q => p)),(q => (s => p))) -> valid ;
coherence
(s => (q => p)) => (q => (s => p)) is valid
by Th8;
end;

theorem Th44: :: LUKASI_1:44
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 by Th15;

theorem :: LUKASI_1:45
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid & q is valid holds
p => r is valid
proof end;

theorem :: LUKASI_1:46
for A being QC-alphabet
for p being Element of CQC-WFF A holds
( p => () is valid & ('not' ()) => p is valid ) by ;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,p,((p => q) => q)) -> valid ;
coherence
p => ((p => q) => q) is valid
by Th7;
end;

registration
let A be QC-alphabet ;
let q, r be Element of CQC-WFF A;
cluster K166(A,(q => (q => r)),(q => r)) -> valid ;
coherence
(q => (q => r)) => (q => r) is valid
by Th10;
end;

theorem :: LUKASI_1:47
for A being QC-alphabet
for q, r being Element of CQC-WFF A st q => (q => r) is valid holds
q => r is valid
proof end;

registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
cluster K166(A,(p => (q => r)),((p => q) => (p => r))) -> valid ;
coherence
(p => (q => r)) => ((p => q) => (p => r)) is valid
by Th11;
end;

theorem Th48: :: LUKASI_1:48
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(p => q) => (p => r) is valid
proof end;

theorem :: LUKASI_1:49
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid & p => q is valid holds
p => r is valid
proof end;

registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
cluster K166(A,((p => q) => r),(q => r)) -> valid ;
coherence
((p => q) => r) => (q => r) is valid
by Th6;
end;

theorem :: LUKASI_1:50
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st (p => q) => r is valid holds
q => r is valid
proof end;

registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
cluster K166(A,(p => q),((r => p) => (r => q))) -> valid ;
coherence
(p => q) => ((r => p) => (r => q)) is valid
by Th9;
end;

theorem :: LUKASI_1:51
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
proof end;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,(p => q),(() => ())) -> valid ;
coherence
(p => q) => (() => ()) is valid
by Th26;
end;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,(() => ()),(q => p)) -> valid ;
coherence
(() => ()) => (q => p) is valid
by Th24;
end;

theorem :: LUKASI_1:52
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( () => () is valid iff q => p is valid )
proof end;

registration
let A be QC-alphabet ;
let p be Element of CQC-WFF A;
cluster K166(A,p,('not' ())) -> valid ;
coherence
p => ('not' ()) is valid
by Th27;
end;

registration
let A be QC-alphabet ;
let p be Element of CQC-WFF A;
cluster K166(A,('not' ()),p) -> valid ;
coherence
('not' ()) => p is valid
by Th25;
end;

theorem :: LUKASI_1:53
for A being QC-alphabet
for p being Element of CQC-WFF A holds
( 'not' () is valid iff p is valid )
proof end;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,(('not' ()) => q),(p => q)) -> valid ;
coherence
(('not' ()) => q) => (p => q) is valid
by Th28;
end;

theorem :: LUKASI_1:54
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ('not' ()) => q is valid iff p => q is valid )
proof end;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,(p => ('not' ())),(p => q)) -> valid ;
coherence
(p => ('not' ())) => (p => q) is valid
by Th29;
end;

theorem :: LUKASI_1:55
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => ('not' ()) is valid iff p => q is valid )
proof end;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,(p => ()),(q => ())) -> valid ;
coherence
(p => ()) => (q => ()) is valid
by Th30;
end;

theorem :: LUKASI_1:56
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p => () is valid holds
q => () is valid
proof end;

registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
cluster K166(A,(() => q),(() => p)) -> valid ;
coherence
(() => q) => (() => p) is valid
by Th31;
end;

theorem :: LUKASI_1:57
for A being QC-alphabet
for p, q being Element of CQC-WFF A st () => q is valid holds
() => p is valid
proof end;

theorem :: LUKASI_1:58
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of () st X |- p => q holds
X |- (q => r) => (p => r)
proof end;

theorem Th59: :: LUKASI_1:59
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of () st X |- p => q & X |- q => r holds
X |- p => r
proof end;

theorem :: LUKASI_1:60
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of () holds X |- p => p by CQC_THE1:59;

theorem :: LUKASI_1:61
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () st X |- p holds
X |- q => p
proof end;

theorem :: LUKASI_1:62
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () st X |- p holds
X |- (p => q) => q
proof end;

theorem Th63: :: LUKASI_1:63
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of () st X |- p => (q => r) holds
X |- q => (p => r)
proof end;

theorem :: LUKASI_1:64
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of () st X |- p => (q => r) & X |- q holds
X |- p => r
proof end;

theorem :: LUKASI_1:65
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () st X |- p => (p => q) holds
X |- p => q
proof end;

theorem :: LUKASI_1:66
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of () st X |- (p => q) => r holds
X |- q => r
proof end;

theorem Th67: :: LUKASI_1:67
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of () st X |- p => (q => r) holds
X |- (p => q) => (p => r)
proof end;

theorem :: LUKASI_1:68
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of () st X |- p => (q => r) & X |- p => q holds
X |- p => r
proof end;

theorem :: LUKASI_1:69
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () holds
( X |- () => () iff X |- q => p )
proof end;

theorem :: LUKASI_1:70
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of () holds
( X |- 'not' () iff X |- p )
proof end;

theorem :: LUKASI_1:71
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () holds
( X |- p => ('not' ()) iff X |- p => q )
proof end;

theorem :: LUKASI_1:72
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () holds
( X |- ('not' ()) => q iff X |- p => q )
proof end;

theorem Th73: :: LUKASI_1:73
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () st X |- p => () holds
X |- q => ()
proof end;

theorem Th74: :: LUKASI_1:74
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () st X |- () => q holds
X |- () => p
proof end;

theorem :: LUKASI_1:75
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () st X |- p => () & X |- q holds
X |- 'not' p
proof end;

theorem :: LUKASI_1:76
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of () st X |- () => q & X |- 'not' q holds
X |- p
proof end;