Negation_introduction
Negation introduction
Logical rule of inference
Negation introduction is a rule of inference, or transformation rule, in the field of propositional calculus.
Negation introduction states that if a given antecedent implies both the consequent and its complement, then the antecedent is a contradiction.[1][2]