This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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