Axiom ax-in2 615

Description: 'Not' elimination. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)

Assertion

Ref	Expression
ax-in2	⊢ (¬ 𝜑 → (𝜑 → 𝜓))

Detailed syntax breakdown of Axiom ax-in2

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

This axiom is referenced by:  pm2.21  617  con2d  624  imorr  721  dcim  841  condcOLD  854  pm5.14dc  911  pm5.54dc  918  mon  2055  difin  3372  indifdir  3391  sosng  4699  iotanul  5193