let X be Subset of MC-wff; :: thesis:
let p be Element of MC-wff ; :: according to INTPRO_1:def 22 :: thesis:
let q, r be Element of MC-wff ; :: thesis:
thus p => (q => p) in CnS4 X by Th82; :: thesis:
thus (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X by Th82; :: thesis:
thus (p '&' q) => p in CnS4 X by Th82; :: thesis:
thus (p '&' q) => q in CnS4 X by Th82; :: thesis:
thus p => (q => (p '&' q)) in CnS4 X by Th82; :: thesis:
thus p => (p 'or' q) in CnS4 X by Th82; :: thesis:
thus q => (p 'or' q) in CnS4 X by Th82; :: thesis:
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X by Th82; :: thesis:
thus FALSUM => p in CnS4 X by Th82; :: thesis:
thus p 'or' (p => FALSUM) in CnS4 X by Th82; :: thesis:
thus (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X by Th84; :: thesis:
thus (Nes p) => p in CnS4 X by Th85; :: thesis:
thus (Nes p) => (Nes (Nes p)) in CnS4 X by Th86; :: thesis:
thus ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) by Th83; :: thesis:
thus ( p in CnS4 X implies Nes p in CnS4 X ) by Th87; :: thesis: