Negated conditional rule

The negated conditional rule is a rule in logic which states that "not (if P then Q)" is equivalent to "P and not Q".

The negated conditional law may be formally stated as:

¬(α → β) is equivalent to α ∧ ¬β

Proof of the negated conditional rule

To prove the negated conditional rule, we will show that ¬(P → Q) implies (P ∧ ¬Q):

1 ¬(P → Q) Pr.
2 ¬P AIP
RTP Contradiction
3 P ACP
RTP Q
4 P ∨ Q ∨I, 2
5 Q ∨E, 2, 4
6 P → Q →I, 3-5
7 ¬(P → Q) R, 1
8 P ¬E, 2-7
9 Q AIP
RTP Contradiction
10 P ACP
RTP Q
11 Q R, 9
12 P → Q →I, 10-11
13 ¬(P → Q) R, 1
14 ¬Q ¬I, 9-13
15 P ∧ ¬Q ¬E, 8, 14