Axiom ax-in2 618

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

Assertion

Ref	Expression
ax-in2	|- ( -. ph -> ( ph -> ps ) )

Detailed syntax breakdown of Axiom ax-in2

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2	1	wn 3	. 2 wff -. ph
3		wps	. . 3 wff ps
4	1, 3	wi 4	. 2 wff ( ph -> ps )
5	2, 4	wi 4	1 wff ( -. ph -> ( ph -> ps ) )

This axiom is referenced by:  pm2.21  620  con2d  627  imorr  726  dcim  846  condcOLD  859  pm5.14dc  916  pm5.54dc  923  ifp2  986  mon  2106  difin  3441  indifdir  3460  sosng  4792  iotanul  5294