Negation introduction

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.

Formal notation

This can be written as:
An example of its use would be an attempt to prove two contradictory statements from a single fact. For example, if a person were to state "Whenever I hear the phone ringing I am happy" and then state "Whenever I hear the phone ringing I am not happy", one can infer that the person never hears the phone ringing.
Many proofs by contradiction use negation introduction as reasoning scheme: to prove ¬P, assume for contradiction P, then derive from it two contradictory inferences Q and ¬Q. Since the latter contradiction renders P impossible, ¬P must hold.

Proof

With identified as, the principle is as a special case of Frege's theorem, already in minimal logic.
Another derivation makes use of as the curried, equivalent form of. Using this twice, the principle is seen equivalent to the negation of
which, via modus ponens and rules for conjunctions, is itself equivalent to the valid noncontradiction principle for.
A classical derivation passing through the introduction of a disjunction may be given as follows:

Step	Proposition	Derivation
1		Given
2		Classical equivalence of the material implication
3		Distributivity
4		Law of noncontradiction for
5		Disjunctive syllogism