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	|- ( ph -> E. x ps )
	bnj1304.2	|- ( ps -> ch )
	bnj1304.3	|- ( ps -> -. ch )
Assertion	bnj1304	|- -. ph

Proof

Step	Hyp	Ref	Expression
1		bnj1304.1	|- ( ph -> E. x ps )
2		bnj1304.2	|- ( ps -> ch )
3		bnj1304.3	|- ( ps -> -. ch )
4		notnotb	|- ( A. x ( ch \/ -. ch ) <-> -. -. A. x ( ch \/ -. ch ) )
5		notnotb	|- ( ch <-> -. -. ch )
6	5	anbi2i	|- ( ( -. ch /\ ch ) <-> ( -. ch /\ -. -. ch ) )
7	6	exbii	|- ( E. x ( -. ch /\ ch ) <-> E. x ( -. ch /\ -. -. ch ) )
8		ioran	|- ( -. ( ch \/ -. ch ) <-> ( -. ch /\ -. -. ch ) )
9	8	exbii	|- ( E. x -. ( ch \/ -. ch ) <-> E. x ( -. ch /\ -. -. ch ) )
10		exnal	|- ( E. x -. ( ch \/ -. ch ) <-> -. A. x ( ch \/ -. ch ) )
11	7 9 10	3bitr2ri	|- ( -. A. x ( ch \/ -. ch ) <-> E. x ( -. ch /\ ch ) )
12	11	notbii	|- ( -. -. A. x ( ch \/ -. ch ) <-> -. E. x ( -. ch /\ ch ) )
13		exancom	|- ( E. x ( -. ch /\ ch ) <-> E. x ( ch /\ -. ch ) )
14	13	notbii	|- ( -. E. x ( -. ch /\ ch ) <-> -. E. x ( ch /\ -. ch ) )
15	4 12 14	3bitri	|- ( A. x ( ch \/ -. ch ) <-> -. E. x ( ch /\ -. ch ) )
16		exmid	|- ( ch \/ -. ch )
17	15 16	mpgbi	|- -. E. x ( ch /\ -. ch )
18	2 3	jca	|- ( ps -> ( ch /\ -. ch ) )
19	1 18	bnj593	|- ( ph -> E. x ( ch /\ -. ch ) )
20	17 19	mto	|- -. ph