ax-in1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ax-in1		Unicode version

Axiom ax-in1 614

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

**Assertion**
Ref	Expression
ax-in1

**Detailed syntax breakdown of Axiom ax-in1**
Step	Hyp	Ref	Expression
1		wph	. . 3
2	1	wn 3	. . 3
3	1, 2	wi 4	. 2
4	3, 2	wi 4	1

Colors of variables: wff set class

This axiom is referenced by: pm2.01 616

W3C validator