Axiom ax-in1 609

Description: 'Not' introduction. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias pm2.01 611 instead. (New usage is discouraged.)

Assertion

Ref	Expression
ax-in1	⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)

Detailed syntax breakdown of Axiom ax-in1

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wn 3	. . 3 wff ¬ 𝜑
3	1, 2	wi 4	. 2 wff (𝜑 → ¬ 𝜑)
4	3, 2	wi 4	1 wff ((𝜑 → ¬ 𝜑) → ¬ 𝜑)

This axiom is referenced by:  pm2.01  611