Negation introduction

Negation introduction
Type	Rule of inference
Field	Propositional calculus
Statement	If a given antecedent implies both the consequent and its complement, then the antecedent is a contradiction.
Symbolic statement	$(P\rightarrow Q)\land (P\rightarrow \neg Q)\rightarrow \neg P$

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 this implies the negated antecedent.