とする．このとき，次が成立する．
(1)
(ア)
(イ)
(2)
(ア)
(イ)
(証明)
(1)
(ア) を示す．
を仮定する．このとき，∨-導入より
i.e.
を得る．したがって，→-導入から(ア)が示された．
(イ) (ア)と同様に示される．
(2)
(ア) を示す．
を仮定する．このとき
に対して∧-除去を適用すれば
を得る．それゆえ，→-導入から(ア)がいえる．
(イ) (ア)と同様．▢
とする．このとき，次が成立する．
(1)
(ア)
(イ)
(2)
(ア)
(イ)
(証明)
(1)
(ア) を示す．
を仮定する．このとき，∨-導入より
i.e.
を得る．したがって，→-導入から(ア)が示された．
(イ) (ア)と同様に示される．
(2)
(ア) を示す．
を仮定する．このとき
に対して∧-除去を適用すれば
を得る．それゆえ，→-導入から(ア)がいえる．
(イ) (ア)と同様．▢