let X be Subset of MC-wff; :: thesis: CnIPC X is IPC_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def 14 :: thesis: for q, r being Element of MC-wff holds
( p => (q => p) in CnIPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
let q, r be Element of MC-wff ; :: thesis: ( p => (q => p) in CnIPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus p => (q => p) in CnIPC X by Th1; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Th2; :: thesis: ( (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p '&' q) => p in CnIPC X by Th3; :: thesis: ( (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p '&' q) => q in CnIPC X by Th4; :: thesis: ( p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus p => (q => (p '&' q)) in CnIPC X by Th5; :: thesis: ( p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus p => (p 'or' q) in CnIPC X by Th6; :: thesis: ( q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus q => (p 'or' q) in CnIPC X by Th7; :: thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Th8; :: thesis: ( FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus FALSUM => p in CnIPC X by Th9; :: thesis: ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X )
thus ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) by Th10; :: thesis: verum