# Metamath Proof Explorer

## Theorem vk15.4jVD

Description: The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 15 Excercise 4.f. found in the "Answers to Starred Exercises" on page 442 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j is vk15.4jVD without virtual deductions and was automatically derived from vk15.4jVD . Step numbers greater than 25 are additional steps necessary for the sequent calculus proof not contained in the Fitch-style proof. Otherwise, step i of the User's Proof corresponds to step i of the Fitch-style proof.

 h1:: |- -. ( E. x -. ph /\ E. x ( ps /\ -. ch ) ) h2:: |- ( A. x ch -> -. E. x ( th /\ ta ) ) h3:: |- -. A. x ( ta -> ph ) 4:: |- (. -. E. x -. th ->. -. E. x -. th ). 5:4: |- (. -. E. x -. th ->. A. x th ). 6:3: |- E. x ( ta /\ -. ph ) 7:: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ( ta /\ -. ph ) ). 8:7: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ta ). 9:7: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. ph ). 10:5: |- (. -. E. x -. th ->. th ). 11:10,8: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ( th /\ ta ) ). 12:11: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. E. x ( th /\ ta ) ). 13:12: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. -. E. x ( th /\ ta ) ). 14:2,13: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. A. x ch ). 140:: |- ( E. x -. th -> A. x E. x -. th ) 141:140: |- ( -. E. x -. th -> A. x -. E. x -. th ) 142:: |- ( A. x ch -> A. x A. x ch ) 143:142: |- ( -. A. x ch -> A. x -. A. x ch ) 144:6,14,141,143: |- (. -. E. x -. th ->. -. A. x ch ). 15:1: |- ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) ) 16:9: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. E. x -. ph ). 161:: |- ( E. x -. ph -> A. x E. x -. ph ) 162:6,16,141,161: |- (. -. E. x -. th ->. E. x -. ph ). 17:162: |- (. -. E. x -. th ->. -. -. E. x -. ph ). 18:15,17: |- (. -. E. x -. th ->. -. E. x ( ps /\ -. ch ) ). 19:18: |- (. -. E. x -. th ->. A. x ( ps -> ch ) ). 20:144: |- (. -. E. x -. th ->. E. x -. ch ). 21:: |- (. -. E. x -. th ,. -. ch ->. -. ch ). 22:19: |- (. -. E. x -. th ->. ( ps -> ch ) ). 23:21,22: |- (. -. E. x -. th ,. -. ch ->. -. ps ). 24:23: |- (. -. E. x -. th ,. -. ch ->. E. x -. ps ). 240:: |- ( E. x -. ps -> A. x E. x -. ps ) 241:20,24,141,240: |- (. -. E. x -. th ->. E. x -. ps ). 25:241: |- (. -. E. x -. th ->. -. A. x ps ). qed:25: |- ( -. E. x -. th -> -. A. x ps )
(Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vk15.4jVD.1 ${⊢}¬\left(\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)$
vk15.4jVD.2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)$
vk15.4jVD.3 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\tau }\to {\phi }\right)$
Assertion vk15.4jVD ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 vk15.4jVD.1 ${⊢}¬\left(\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)$
2 vk15.4jVD.2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)$
3 vk15.4jVD.3 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\tau }\to {\phi }\right)$
4 exanali ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\tau }\wedge ¬{\phi }\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\tau }\to {\phi }\right)$
5 4 biimpri ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\tau }\to {\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\tau }\wedge ¬{\phi }\right)$
6 3 5 e0a ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\tau }\wedge ¬{\phi }\right)$
7 idn1 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }\right)$
8 alex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\theta }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }$
9 8 biimpri ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\theta }$
10 7 9 e1a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }\forall {x}\phantom{\rule{.4em}{0ex}}{\theta }\right)$
11 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\theta }\to {\theta }$
12 10 11 e1a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }{\theta }\right)$
13 idn2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }\left({\tau }\wedge ¬{\phi }\right)\right)$
14 simpl ${⊢}\left({\tau }\wedge ¬{\phi }\right)\to {\tau }$
15 13 14 e2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }{\tau }\right)$
16 pm3.2 ${⊢}{\theta }\to \left({\tau }\to \left({\theta }\wedge {\tau }\right)\right)$
17 12 15 16 e12 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }\left({\theta }\wedge {\tau }\right)\right)$
18 19.8a ${⊢}\left({\theta }\wedge {\tau }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)$
19 17 18 e2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)\right)$
20 notnot ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)\to ¬¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)$
21 19 20 e2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }¬¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)\right)$
22 con3 ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)\right)\to \left(¬¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\theta }\wedge {\tau }\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
23 2 21 22 e02 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }¬\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
24 hbe1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }\to \forall {x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }$
25 24 hbn ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }$
26 hba1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }$
27 26 hbn ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }$
28 6 23 25 27 exinst01 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }¬\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
29 exnal ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\chi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }$
30 29 biimpri ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{\chi }$
31 28 30 e1a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }\exists {x}\phantom{\rule{.4em}{0ex}}¬{\chi }\right)$
32 idn2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}¬{\chi }{\to }¬{\chi }\right)$
33 pm3.13 ${⊢}¬\left(\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)\to \left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\vee ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)$
34 1 33 e0a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\vee ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)$
35 simpr ${⊢}\left({\tau }\wedge ¬{\phi }\right)\to ¬{\phi }$
36 13 35 e2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }¬{\phi }\right)$
37 19.8a ${⊢}¬{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
38 36 37 e2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}\left({\tau }\wedge ¬{\phi }\right){\to }\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
39 hbe1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
40 6 38 25 39 exinst01 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
41 notnot ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to ¬¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
42 40 41 e1a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }¬¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
43 pm2.53 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\vee ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)\to \left(¬¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)$
44 34 42 43 e01 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\right)$
45 exanali ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)$
46 45 con5i ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ¬{\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)$
47 44 46 e1a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)\right)$
48 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)\to \left({\psi }\to {\chi }\right)$
49 47 48 e1a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }\left({\psi }\to {\chi }\right)\right)$
50 con3 ${⊢}\left({\psi }\to {\chi }\right)\to \left(¬{\chi }\to ¬{\psi }\right)$
51 50 com12 ${⊢}¬{\chi }\to \left(\left({\psi }\to {\chi }\right)\to ¬{\psi }\right)$
52 32 49 51 e21 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}¬{\chi }{\to }¬{\psi }\right)$
53 19.8a ${⊢}¬{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
54 52 53 e2 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{,}¬{\chi }{\to }\exists {x}\phantom{\rule{.4em}{0ex}}¬{\psi }\right)$
55 hbe1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
56 31 54 25 55 exinst11 ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }\exists {x}\phantom{\rule{.4em}{0ex}}¬{\psi }\right)$
57 exnal ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\psi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
58 57 biimpi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\psi }\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
59 56 58 e1a ${⊢}\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }{\to }¬\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
60 59 in1 ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}¬{\theta }\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$