Metamath Proof Explorer

Theorem vk15.4j

Description: Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j is vk15.4jVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vk15.4j.1 
|- -. ( E. x -. ph /\ E. x ( ps /\ -. ch ) )
vk15.4j.2 
|- ( A. x ch -> -. E. x ( th /\ ta ) )
vk15.4j.3 
|- -. A. x ( ta -> ph )
Assertion vk15.4j 
|- ( -. E. x -. th -> -. A. x ps )

Proof

Step Hyp Ref Expression
1 vk15.4j.1 
 |-  -. ( E. x -. ph /\ E. x ( ps /\ -. ch ) )
2 vk15.4j.2 
 |-  ( A. x ch -> -. E. x ( th /\ ta ) )
3 vk15.4j.3 
 |-  -. A. x ( ta -> ph )
4 exanali 
 |-  ( E. x ( ta /\ -. ph ) <-> -. A. x ( ta -> ph ) )
5 3 4 mpbir 
 |-  E. x ( ta /\ -. ph )
6 alex 
 |-  ( A. x th <-> -. E. x -. th )
7 6 biimpri 
 |-  ( -. E. x -. th -> A. x th )
8 7 19.21bi 
 |-  ( -. E. x -. th -> th )
9 simpl 
 |-  ( ( ta /\ -. ph ) -> ta )
10 9 a1i 
 |-  ( -. E. x -. th -> ( ( ta /\ -. ph ) -> ta ) )
11 19.8a 
 |-  ( ( th /\ ta ) -> E. x ( th /\ ta ) )
12 8 10 11 syl6an 
 |-  ( -. E. x -. th -> ( ( ta /\ -. ph ) -> E. x ( th /\ ta ) ) )
13 notnot 
 |-  ( E. x ( th /\ ta ) -> -. -. E. x ( th /\ ta ) )
14 12 13 syl6 
 |-  ( -. E. x -. th -> ( ( ta /\ -. ph ) -> -. -. E. x ( th /\ ta ) ) )
15 con3 
 |-  ( ( A. x ch -> -. E. x ( th /\ ta ) ) -> ( -. -. E. x ( th /\ ta ) -> -. A. x ch ) )
16 2 14 15 mpsylsyld 
 |-  ( -. E. x -. th -> ( ( ta /\ -. ph ) -> -. A. x ch ) )
17 hbe1 
 |-  ( E. x -. th -> A. x E. x -. th )
18 17 hbn 
 |-  ( -. E. x -. th -> A. x -. E. x -. th )
19 hbn1 
 |-  ( -. A. x ch -> A. x -. A. x ch )
20 5 16 18 19 eexinst01 
 |-  ( -. E. x -. th -> -. A. x ch )
21 exnal 
 |-  ( E. x -. ch <-> -. A. x ch )
22 20 21 sylibr 
 |-  ( -. E. x -. th -> E. x -. ch )
23 pm3.13 
 |-  ( -. ( E. x -. ph /\ E. x ( ps /\ -. ch ) ) -> ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) ) )
24 1 23 ax-mp 
 |-  ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) )
25 simpr 
 |-  ( ( ta /\ -. ph ) -> -. ph )
26 25 a1i 
 |-  ( -. E. x -. th -> ( ( ta /\ -. ph ) -> -. ph ) )
27 19.8a 
 |-  ( -. ph -> E. x -. ph )
28 26 27 syl6 
 |-  ( -. E. x -. th -> ( ( ta /\ -. ph ) -> E. x -. ph ) )
29 hbe1 
 |-  ( E. x -. ph -> A. x E. x -. ph )
30 5 28 18 29 eexinst01 
 |-  ( -. E. x -. th -> E. x -. ph )
31 notnot 
 |-  ( E. x -. ph -> -. -. E. x -. ph )
32 30 31 syl 
 |-  ( -. E. x -. th -> -. -. E. x -. ph )
33 pm2.53 
 |-  ( ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) ) -> ( -. -. E. x -. ph -> -. E. x ( ps /\ -. ch ) ) )
34 24 32 33 mpsyl 
 |-  ( -. E. x -. th -> -. E. x ( ps /\ -. ch ) )
35 exanali 
 |-  ( E. x ( ps /\ -. ch ) <-> -. A. x ( ps -> ch ) )
36 35 con5i 
 |-  ( -. E. x ( ps /\ -. ch ) -> A. x ( ps -> ch ) )
37 34 36 syl 
 |-  ( -. E. x -. th -> A. x ( ps -> ch ) )
38 37 19.21bi 
 |-  ( -. E. x -. th -> ( ps -> ch ) )
39 38 con3d 
 |-  ( -. E. x -. th -> ( -. ch -> -. ps ) )
40 19.8a 
 |-  ( -. ps -> E. x -. ps )
41 39 40 syl6 
 |-  ( -. E. x -. th -> ( -. ch -> E. x -. ps ) )
42 hbe1 
 |-  ( E. x -. ps -> A. x E. x -. ps )
43 22 41 18 42 eexinst11 
 |-  ( -. E. x -. th -> E. x -. ps )
44 exnal 
 |-  ( E. x -. ps <-> -. A. x ps )
45 43 44 sylib 
 |-  ( -. E. x -. th -> -. A. x ps )