演繹定理の証明は良く分析すると
式変形を実際に書き出せるようになってるから
援用すれば良いんじゃないかと思うけどね