Theorem bnj1304

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1304.1	$$⊢\phi \to \exists x\psi$$
	bnj1304.2	$$⊢\psi \to \chi$$
	bnj1304.3	$$⊢\psi \to \neg \chi$$
Assertion	bnj1304	$$⊢\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		bnj1304.1	$$⊢\phi \to \exists x\psi$$
2		bnj1304.2	$$⊢\psi \to \chi$$
3		bnj1304.3	$$⊢\psi \to \neg \chi$$
4		notnotb	$$⊢\forall x\left(\chi \vee \neg \chi \right)\leftrightarrow \neg \neg \forall x\left(\chi \vee \neg \chi \right)$$
5		notnotb	$$⊢\chi \leftrightarrow \neg \neg \chi$$
6	5	anbi2i	$$⊢\left(\neg \chi \wedge \chi \right)\leftrightarrow \left(\neg \chi \wedge \neg \neg \chi \right)$$
7	6	exbii	$$⊢\exists x\left(\neg \chi \wedge \chi \right)\leftrightarrow \exists x\left(\neg \chi \wedge \neg \neg \chi \right)$$
8		ioran	$$⊢\neg \left(\chi \vee \neg \chi \right)\leftrightarrow \left(\neg \chi \wedge \neg \neg \chi \right)$$
9	8	exbii	$$⊢\exists x\neg \left(\chi \vee \neg \chi \right)\leftrightarrow \exists x\left(\neg \chi \wedge \neg \neg \chi \right)$$
10		exnal	$$⊢\exists x\neg \left(\chi \vee \neg \chi \right)\leftrightarrow \neg \forall x\left(\chi \vee \neg \chi \right)$$
11	7 9 10	3bitr2ri	$$⊢\neg \forall x\left(\chi \vee \neg \chi \right)\leftrightarrow \exists x\left(\neg \chi \wedge \chi \right)$$
12	11	notbii	$$⊢\neg \neg \forall x\left(\chi \vee \neg \chi \right)\leftrightarrow \neg \exists x\left(\neg \chi \wedge \chi \right)$$
13		exancom	$$⊢\exists x\left(\neg \chi \wedge \chi \right)\leftrightarrow \exists x\left(\chi \wedge \neg \chi \right)$$
14	13	notbii	$$⊢\neg \exists x\left(\neg \chi \wedge \chi \right)\leftrightarrow \neg \exists x\left(\chi \wedge \neg \chi \right)$$
15	4 12 14	3bitri	$$⊢\forall x\left(\chi \vee \neg \chi \right)\leftrightarrow \neg \exists x\left(\chi \wedge \neg \chi \right)$$
16		exmid	$$⊢\left(\chi \vee \neg \chi \right)$$
17	15 16	mpgbi	$$⊢\neg \exists x\left(\chi \wedge \neg \chi \right)$$
18	2 3	jca	$$⊢\psi \to \left(\chi \wedge \neg \chi \right)$$
19	1 18	bnj593	$$⊢\phi \to \exists x\left(\chi \wedge \neg \chi \right)$$
20	17 19	mto	$$⊢\neg \phi$$