:: by Grzegorz Bancerek, Agata Darmochwa\l and Andrzej Trybulec

::

:: Received September 26, 1990

:: Copyright (c) 1990-2019 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

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

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

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;

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 ((('not' p) => 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 => (((('not' 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 => ((('not' p) => p) => p)) => ((('not' 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 => ((('not' p) => p) => p) in TAUT A

proof end;

Lm9: for A being QC-alphabet

for p, q, t being Element of CQC-WFF A holds (('not' p) => 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) => ((('not' p) => q) => r) in TAUT A

proof end;

Lm11: for A being QC-alphabet

for p, q being Element of CQC-WFF A holds (('not' p) => 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 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

for p, q, r being Element of CQC-WFF A holds ((p => q) => r) => (q => r) 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

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

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

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

for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p => q) => (p => r)) 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

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

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

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

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

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

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

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

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

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 => (VERUM A) in TAUT A by Th13, CQC_THE1:41;

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

Lm23: for A being QC-alphabet

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

proof end;

Lm24: for A being QC-alphabet

for p being Element of CQC-WFF A holds (('not' p) => ('not' (VERUM A))) => 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 (('not' p) => ('not' q)) => (q => p) in TAUT A

for p, q being Element of CQC-WFF A holds (('not' p) => ('not' q)) => (q => 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' (VERUM A))) => ('not' p) in TAUT A

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

let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds (p => ('not' (VERUM A))) => ('not' p) in TAUT A

let p be Element of CQC-WFF A; :: thesis: (p => ('not' (VERUM A))) => ('not' p) in TAUT A

('not' ('not' p)) => p in TAUT A by Th25;

then A1: (p => ('not' (VERUM A))) => (('not' ('not' p)) => ('not' (VERUM A))) in TAUT A by Th2;

(('not' ('not' p)) => ('not' (VERUM A))) => ('not' p) in TAUT A by Lm24;

hence (p => ('not' (VERUM A))) => ('not' p) in TAUT A by A1, Th3; :: thesis: verum

end;
let p be Element of CQC-WFF A; :: thesis: (p => ('not' (VERUM A))) => ('not' p) in TAUT A

('not' ('not' p)) => p in TAUT A by Th25;

then A1: (p => ('not' (VERUM A))) => (('not' ('not' p)) => ('not' (VERUM A))) in TAUT A by Th2;

(('not' ('not' p)) => ('not' (VERUM A))) => ('not' p) in TAUT A by Lm24;

hence (p => ('not' (VERUM A))) => ('not' p) in TAUT A by A1, Th3; :: thesis: verum

theorem Th26: :: LUKASI_1:26

for A being QC-alphabet

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

for p, q being Element of CQC-WFF A holds (p => q) => (('not' q) => ('not' p)) 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' ('not' p)) => q) => (p => q) in TAUT A & (p => q) => (('not' ('not' p)) => q) in TAUT A )

for p, q being Element of CQC-WFF A holds

( (('not' ('not' p)) => q) => (p => q) in TAUT A & (p => q) => (('not' ('not' p)) => 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' ('not' q))) => (p => q) in TAUT A & (p => q) => (p => ('not' ('not' q))) in TAUT A )

for p, q being Element of CQC-WFF A holds

( (p => ('not' ('not' q))) => (p => q) in TAUT A & (p => q) => (p => ('not' ('not' q))) 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 => ('not' q)) => (q => ('not' p)) in TAUT A

for p, q being Element of CQC-WFF A holds (p => ('not' q)) => (q => ('not' p)) 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 (('not' p) => q) => (('not' q) => p) in TAUT A

for p, q being Element of CQC-WFF A holds (('not' p) => q) => (('not' 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 => ('not' p)) => ('not' p) in TAUT A

for p being Element of CQC-WFF A holds (p => ('not' p)) => ('not' p) 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 ('not' q) => ('not' p) in TAUT A )

for p, q being Element of CQC-WFF A holds

( p => q in TAUT A iff ('not' q) => ('not' p) in TAUT A )

proof end;

theorem :: LUKASI_1:35

theorem :: LUKASI_1:36

for A being QC-alphabet

for p being Element of CQC-WFF A holds

( p in TAUT A iff 'not' ('not' p) in TAUT A )

for p being Element of CQC-WFF A holds

( p in TAUT A iff 'not' ('not' p) 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' ('not' q)) in TAUT A )

for p, q being Element of CQC-WFF A holds

( p => q in TAUT A iff p => ('not' ('not' q)) 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' ('not' p)) => q in TAUT A )

for p, q being Element of CQC-WFF A holds

( p => q in TAUT A iff ('not' ('not' p)) => 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 => ('not' q) in TAUT A holds

q => ('not' p) in TAUT A

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

q => ('not' p) in TAUT A

proof end;

theorem :: LUKASI_1:40

for A being QC-alphabet

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

('not' q) => p in TAUT A

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

('not' q) => 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;

coherence

(p => q) => ((q => r) => (p => r)) is valid by Th1;

end;
let p, q, r be Element of CQC-WFF A;

coherence

(p => q) => ((q => r) => (p => r)) is valid by Th1;

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

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

(q => r) => (p => r) is valid

proof end;

registration
end;

registration
end;

theorem :: LUKASI_1:43

registration

let A be QC-alphabet ;

let p, q, s be Element of CQC-WFF A;

coherence

(s => (q => p)) => (q => (s => p)) is valid by Th8;

end;
let p, q, s be Element of CQC-WFF A;

coherence

(s => (q => p)) => (q => (s => p)) is valid by Th8;

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

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

registration

let A be QC-alphabet ;

let p, q be Element of CQC-WFF A;

coherence

p => ((p => q) => q) is valid by Th7;

end;
let p, q be Element of CQC-WFF A;

coherence

p => ((p => q) => q) is valid by Th7;

registration

let A be QC-alphabet ;

let q, r be Element of CQC-WFF A;

coherence

(q => (q => r)) => (q => r) is valid by Th10;

end;
let q, r be Element of CQC-WFF A;

coherence

(q => (q => r)) => (q => r) is valid by Th10;

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

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;

coherence

(p => (q => r)) => ((p => q) => (p => r)) is valid by Th11;

end;
let p, q, r be Element of CQC-WFF A;

coherence

(p => (q => r)) => ((p => q) => (p => r)) is valid by Th11;

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

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

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;

coherence

((p => q) => r) => (q => r) is valid by Th6;

end;
let p, q, r be Element of CQC-WFF A;

coherence

((p => q) => r) => (q => r) is valid by Th6;

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

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;

coherence

(p => q) => ((r => p) => (r => q)) is valid by Th9;

end;
let p, q, r be Element of CQC-WFF A;

coherence

(p => q) => ((r => p) => (r => q)) is valid by Th9;

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

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;

coherence

(p => q) => (('not' q) => ('not' p)) is valid by Th26;

end;
let p, q be Element of CQC-WFF A;

coherence

(p => q) => (('not' q) => ('not' p)) is valid by Th26;

registration

let A be QC-alphabet ;

let p, q be Element of CQC-WFF A;

coherence

(('not' p) => ('not' q)) => (q => p) is valid by Th24;

end;
let p, q be Element of CQC-WFF A;

coherence

(('not' p) => ('not' q)) => (q => p) is valid by Th24;

theorem :: LUKASI_1:52

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( ('not' p) => ('not' q) is valid iff q => p is valid )

for p, q being Element of CQC-WFF A holds

( ('not' p) => ('not' q) is valid iff q => p is valid )

proof end;

registration

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

coherence

p => ('not' ('not' p)) is valid by Th27;

end;
let p be Element of CQC-WFF A;

coherence

p => ('not' ('not' p)) is valid by Th27;

registration

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

coherence

('not' ('not' p)) => p is valid by Th25;

end;
let p be Element of CQC-WFF A;

coherence

('not' ('not' p)) => p is valid by Th25;

theorem :: LUKASI_1:53

for A being QC-alphabet

for p being Element of CQC-WFF A holds

( 'not' ('not' p) is valid iff p is valid )

for p being Element of CQC-WFF A holds

( 'not' ('not' p) is valid iff p is valid )

proof end;

registration

let A be QC-alphabet ;

let p, q be Element of CQC-WFF A;

coherence

(('not' ('not' p)) => q) => (p => q) is valid by Th28;

end;
let p, q be Element of CQC-WFF A;

coherence

(('not' ('not' p)) => q) => (p => q) is valid by Th28;

theorem :: LUKASI_1:54

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( ('not' ('not' p)) => q is valid iff p => q is valid )

for p, q being Element of CQC-WFF A holds

( ('not' ('not' p)) => 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;

coherence

(p => ('not' ('not' q))) => (p => q) is valid by Th29;

end;
let p, q be Element of CQC-WFF A;

coherence

(p => ('not' ('not' q))) => (p => q) is valid by Th29;

theorem :: LUKASI_1:55

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( p => ('not' ('not' q)) is valid iff p => q is valid )

for p, q being Element of CQC-WFF A holds

( p => ('not' ('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;

coherence

(p => ('not' q)) => (q => ('not' p)) is valid by Th30;

end;
let p, q be Element of CQC-WFF A;

coherence

(p => ('not' q)) => (q => ('not' p)) is valid by Th30;

theorem :: LUKASI_1:56

for A being QC-alphabet

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

q => ('not' p) is valid

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

q => ('not' p) is valid

proof end;

registration

let A be QC-alphabet ;

let p, q be Element of CQC-WFF A;

coherence

(('not' p) => q) => (('not' q) => p) is valid by Th31;

end;
let p, q be Element of CQC-WFF A;

coherence

(('not' p) => q) => (('not' q) => p) is valid by Th31;

theorem :: LUKASI_1:57

for A being QC-alphabet

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

('not' q) => p is valid

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

('not' q) => 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 (CQC-WFF A) st X |- p => q holds

X |- (q => r) => (p => r)

for p, q, r being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p => q & X |- q => r holds

X |- p => r

for p, q, r being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) holds X |- p => p by CQC_THE1:59;

for p being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p holds

X |- q => p

for p, q being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p holds

X |- (p => q) => q

for p, q being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p => (q => r) holds

X |- q => (p => r)

for p, q, r being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p => (q => r) & X |- q holds

X |- p => r

for p, q, r being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p => (p => q) holds

X |- p => q

for p, q being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- (p => q) => r holds

X |- q => r

for p, q, r being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p => (q => r) holds

X |- (p => q) => (p => r)

for p, q, r being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) st X |- p => (q => r) & X |- p => q holds

X |- p => r

for p, q, r being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) 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 (CQC-WFF A) holds

( X |- ('not' p) => ('not' q) iff X |- q => p )

for p, q being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) holds

( X |- ('not' p) => ('not' q) 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 (CQC-WFF A) holds

( X |- 'not' ('not' p) iff X |- p )

for p being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) holds

( X |- 'not' ('not' p) 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 (CQC-WFF A) holds

( X |- p => ('not' ('not' q)) iff X |- p => q )

for p, q being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) holds

( X |- p => ('not' ('not' q)) 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 (CQC-WFF A) holds

( X |- ('not' ('not' p)) => q iff X |- p => q )

for p, q being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) holds

( X |- ('not' ('not' p)) => 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 (CQC-WFF A) st X |- p => ('not' q) holds

X |- q => ('not' p)

for p, q being Element of CQC-WFF A

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

X |- q => ('not' p)

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 (CQC-WFF A) st X |- ('not' p) => q holds

X |- ('not' q) => p

for p, q being Element of CQC-WFF A

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

X |- ('not' q) => 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 (CQC-WFF A) st X |- p => ('not' q) & X |- q holds

X |- 'not' p

for p, q being Element of CQC-WFF A

for X being Subset of (CQC-WFF A) st X |- p => ('not' q) & 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 (CQC-WFF A) st X |- ('not' p) => q & X |- 'not' q holds

X |- p

for p, q being Element of CQC-WFF A

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

X |- p

proof end;