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	$$⊢\phi$$
Assertion	atnaiana	$$⊢\neg \left(\phi \to \left(\phi \wedge \neg \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		atnaiana.1	$$⊢\phi$$
2	1	bitru	$$⊢\phi \leftrightarrow \top$$
3		pm3.24	$$⊢\neg \left(\phi \wedge \neg \phi \right)$$
4	3	bifal	$$⊢\left(\phi \wedge \neg \phi \right)\leftrightarrow \perp$$
5	2 4	aifftbifffaibif	$$⊢\left(\phi \to \left(\phi \wedge \neg \phi \right)\right)\leftrightarrow \perp$$
6	5	aisfina	$$⊢\neg \left(\phi \to \left(\phi \wedge \neg \phi \right)\right)$$