（p→q）↔（p∨q）
（A→B）→（（C→D）→（A∧C→B∧D））
（（p∧q∧r）→s）→（¬s→（p→（q→¬r）））(https://www.daowen.com)
（¬p∧¬q→r）↔（¬r→p∨q）
（p→q∧r）→（p→q）∧（p→r）
