theorem Th82: :: INTPRO_1:82

for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds
( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )