environ
vocabularies HIDDEN, FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, QC_LANG2, XBOOLEAN, INTPRO_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1;
definitions TARSKI;
theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0;
registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1, NAT_1, XCMPLX_0;
constructors HIDDEN, NAT_1, FINSEQ_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities ;
expansions TARSKI;
Lm1:
for E being set st E is MC-closed holds
not E is empty
Lm2:
for X being Subset of MC-wff holds CnIPC (CnIPC X) c= CnIPC X
Lm3:
for X being Subset of MC-wff holds CnIPC X is IPC_theory
by Th1, Th2, Th3, Th4, Th5, Th6, Th7, Th8, Th9, Th10;
Lm4:
for p, q, r, s being Element of MC-wff holds (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
Lm5:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => q in IPC-Taut
Lm6:
for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut
Lm7:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
Lm8:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
Lm9:
for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
Lm10:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
Lm11:
for p, q, s being Element of MC-wff holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
Lm12:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
Lm13:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
Lm14:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
Lm15:
for p, q, s being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
Lm16:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
Lm17:
for p, q, s being Element of MC-wff holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
Lm18:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
Lm19:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
Lm20:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
Lm21:
for X being Subset of MC-wff holds CnCPC (CnCPC X) c= CnCPC X
Lm22:
for X being Subset of MC-wff holds CnCPC X is CPC_theory
by Th69, Th70;
Lm23:
for X being Subset of MC-wff holds CnS4 (CnS4 X) c= CnS4 X
Lm24:
for X being Subset of MC-wff holds CnS4 X is S4_theory
by Th82, Th84, Th85, Th86, Th83, Th87;