Theorem aibnbna

Description: Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016)

	Ref	Expression
Hypotheses	aibnbna.1	|- ( ph -> ps )
	aibnbna.2	|- -. ps
Assertion	aibnbna	|- -. ph

Proof

Step	Hyp	Ref	Expression
1		aibnbna.1	|- ( ph -> ps )
2		aibnbna.2	|- -. ps
3	2 1	mto	|- -. ph