Theorem T000083

∧ ¬ ⇒ ¬