let X be Subset of MC-wff; :: thesis: CnCPC X is CPC_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def 19 :: thesis: for q, r being Element of MC-wff holds
( p => (q => p) in CnCPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
let q, r be Element of MC-wff ; :: thesis: ( p => (q => p) in CnCPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p => (q => p) in CnCPC X by Th69; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X by Th69; :: thesis: ( (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p '&' q) => p in CnCPC X by Th69; :: thesis: ( (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p '&' q) => q in CnCPC X by Th69; :: thesis: ( p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p => (q => (p '&' q)) in CnCPC X by Th69; :: thesis: ( p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p => (p 'or' q) in CnCPC X by Th69; :: thesis: ( q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus q => (p 'or' q) in CnCPC X by Th69; :: thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X by Th69; :: thesis: ( FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus FALSUM => p in CnCPC X by Th69; :: thesis: ( p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p 'or' (p => FALSUM) in CnCPC X by Th69; :: thesis: ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X )
thus ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) by Th70; :: thesis: verum