let X be Subset of MC-wff; :: thesis: for q, r being Element of MC-wff st X |-_IPC r & X \/ {r} |-_IPC q holds
X |-_IPC q
let q, r be Element of MC-wff ; :: thesis: ( X |-_IPC r & X \/ {r} |-_IPC q implies X |-_IPC q )
assume A1: ( X |-_IPC r & X \/ {r} |-_IPC q ) ; :: thesis: X |-_IPC q
then X |-_IPC r => q by Th53;
hence X |-_IPC q by A1, Th27; :: thesis: verum