Theorem aibnbna 47703

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

Hypotheses

Ref	Expression
aibnbna.1	⊢ (𝜑 → 𝜓)
aibnbna.2	⊢ ¬ 𝜓

Assertion

Ref	Expression
aibnbna	⊢ ¬ 𝜑

Proof of Theorem aibnbna

Step	Hyp	Ref	Expression
1		aibnbna.2	. 2 ⊢ ¬ 𝜓
2		aibnbna.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mto 200	1 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  aibnbaif  47704