この辺の論理展開を形式的に考えたいなら
真理値表のような低レベルなものより
シーケント計算で考えたら?