  This rule is more complex, but it has the same effect as the arrow elimination rule: It says that if \(X\) suffices for \(A\), and if you use \(B\) (in some context \(Y)\) to prove \(C\) then you could just as well have used \(A \rightarrow B\) together with \(X\) (in that same context \(Y)\) to prove \(C\), since \(A \rightarrow B\) together with \(X\) gives you \(B\). 