Theorem atnaiana

Description: Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020)

	Ref	Expression
Hypothesis	atnaiana.1	⊢ 𝜑
Assertion	atnaiana	⊢ ¬ ( 𝜑 → ( 𝜑 ∧ ¬ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		atnaiana.1	⊢ 𝜑
2	1	bitru	⊢ ( 𝜑 ↔ ⊤ )
3		pm3.24	⊢ ¬ ( 𝜑 ∧ ¬ 𝜑 )
4	3	bifal	⊢ ( ( 𝜑 ∧ ¬ 𝜑 ) ↔ ⊥ )
5	2 4	aifftbifffaibif	⊢ ( ( 𝜑 → ( 𝜑 ∧ ¬ 𝜑 ) ) ↔ ⊥ )
6	5	aisfina	⊢ ¬ ( 𝜑 → ( 𝜑 ∧ ¬ 𝜑 ) )