Theorem vk15.4jVD 39150

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 38734 is vk15.4jVD 39150 without virtual deductions and was automatically derived from vk15.4jVD 39150. 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.)

Hypotheses

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

Assertion

Ref	Expression
vk15.4jVD	|- ( -. E. x -. th -> -. A. x ps )

Proof of Theorem vk15.4jVD

Step	Hyp	Ref	Expression
1		vk15.4jVD.3	. . . . . . 7 |- -. A. x ( ta -> ph )
2		exanali 1786	. . . . . . . 8 |- ( E. x ( ta /\ -. ph ) <-> -. A. x ( ta -> ph ) )
3	2	biimpri 218	. . . . . . 7 |- ( -. A. x ( ta -> ph ) -> E. x ( ta /\ -. ph ) )
4	1, 3	e0a 38999	. . . . . 6 |- E. x ( ta /\ -. ph )
5		vk15.4jVD.2	. . . . . . 7 |- ( A. x ch -> -. E. x ( th /\ ta ) )
6		idn1 38790	. . . . . . . . . . . 12 |- (. -. E. x -. th ->. -. E. x -. th ).
7		alex 1753	. . . . . . . . . . . . 13 |- ( A. x th <-> -. E. x -. th )
8	7	biimpri 218	. . . . . . . . . . . 12 |- ( -. E. x -. th -> A. x th )
9	6, 8	e1a 38852	. . . . . . . . . . 11 |- (. -. E. x -. th ->. A. x th ).
10		sp 2053	. . . . . . . . . . 11 |- ( A. x th -> th )
11	9, 10	e1a 38852	. . . . . . . . . 10 |- (. -. E. x -. th ->. th ).
12		idn2 38838	. . . . . . . . . . 11 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ( ta /\ -. ph ) ).
13		simpl 473	. . . . . . . . . . 11 |- ( ( ta /\ -. ph ) -> ta )
14	12, 13	e2 38856	. . . . . . . . . 10 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ta ).
15		pm3.2 463	. . . . . . . . . 10 |- ( th -> ( ta -> ( th /\ ta ) ) )
16	11, 14, 15	e12 38951	. . . . . . . . 9 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ( th /\ ta ) ).
17		19.8a 2052	. . . . . . . . 9 |- ( ( th /\ ta ) -> E. x ( th /\ ta ) )
18	16, 17	e2 38856	. . . . . . . 8 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. E. x ( th /\ ta ) ).
19		notnot 136	. . . . . . . 8 |- ( E. x ( th /\ ta ) -> -. -. E. x ( th /\ ta ) )
20	18, 19	e2 38856	. . . . . . 7 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. -. E. x ( th /\ ta ) ).
21		con3 149	. . . . . . 7 |- ( ( A. x ch -> -. E. x ( th /\ ta ) ) -> ( -. -. E. x ( th /\ ta ) -> -. A. x ch ) )
22	5, 20, 21	e02 38922	. . . . . 6 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. A. x ch ).
23		hbe1 2021	. . . . . . 7 |- ( E. x -. th -> A. x E. x -. th )
24	23	hbn 2146	. . . . . 6 |- ( -. E. x -. th -> A. x -. E. x -. th )
25		hba1 2151	. . . . . . 7 |- ( A. x ch -> A. x A. x ch )
26	25	hbn 2146	. . . . . 6 |- ( -. A. x ch -> A. x -. A. x ch )
27	4, 22, 24, 26	exinst01 38850	. . . . 5 |- (. -. E. x -. th ->. -. A. x ch ).
28		exnal 1754	. . . . . 6 |- ( E. x -. ch <-> -. A. x ch )
29	28	biimpri 218	. . . . 5 |- ( -. A. x ch -> E. x -. ch )
30	27, 29	e1a 38852	. . . 4 |- (. -. E. x -. th ->. E. x -. ch ).
31		idn2 38838	. . . . . 6 |- (. -. E. x -. th ,. -. ch ->. -. ch ).
32		vk15.4jVD.1	. . . . . . . . . 10 |- -. ( E. x -. ph /\ E. x ( ps /\ -. ch ) )
33		pm3.13 522	. . . . . . . . . 10 |- ( -. ( E. x -. ph /\ E. x ( ps /\ -. ch ) ) -> ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) ) )
34	32, 33	e0a 38999	. . . . . . . . 9 |- ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) )
35		simpr 477	. . . . . . . . . . . . 13 |- ( ( ta /\ -. ph ) -> -. ph )
36	12, 35	e2 38856	. . . . . . . . . . . 12 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. ph ).
37		19.8a 2052	. . . . . . . . . . . 12 |- ( -. ph -> E. x -. ph )
38	36, 37	e2 38856	. . . . . . . . . . 11 |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. E. x -. ph ).
39		hbe1 2021	. . . . . . . . . . 11 |- ( E. x -. ph -> A. x E. x -. ph )
40	4, 38, 24, 39	exinst01 38850	. . . . . . . . . 10 |- (. -. E. x -. th ->. E. x -. ph ).
41		notnot 136	. . . . . . . . . 10 |- ( E. x -. ph -> -. -. E. x -. ph )
42	40, 41	e1a 38852	. . . . . . . . 9 |- (. -. E. x -. th ->. -. -. E. x -. ph ).
43		pm2.53 388	. . . . . . . . 9 |- ( ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) ) -> ( -. -. E. x -. ph -> -. E. x ( ps /\ -. ch ) ) )
44	34, 42, 43	e01 38916	. . . . . . . 8 |- (. -. E. x -. th ->. -. E. x ( ps /\ -. ch ) ).
45		exanali 1786	. . . . . . . . 9 |- ( E. x ( ps /\ -. ch ) <-> -. A. x ( ps -> ch ) )
46	45	con5i 38729	. . . . . . . 8 |- ( -. E. x ( ps /\ -. ch ) -> A. x ( ps -> ch ) )
47	44, 46	e1a 38852	. . . . . . 7 |- (. -. E. x -. th ->. A. x ( ps -> ch ) ).
48		sp 2053	. . . . . . 7 |- ( A. x ( ps -> ch ) -> ( ps -> ch ) )
49	47, 48	e1a 38852	. . . . . 6 |- (. -. E. x -. th ->. ( ps -> ch ) ).
50		con3 149	. . . . . . 7 |- ( ( ps -> ch ) -> ( -. ch -> -. ps ) )
51	50	com12 32	. . . . . 6 |- ( -. ch -> ( ( ps -> ch ) -> -. ps ) )
52	31, 49, 51	e21 38957	. . . . 5 |- (. -. E. x -. th ,. -. ch ->. -. ps ).
53		19.8a 2052	. . . . 5 |- ( -. ps -> E. x -. ps )
54	52, 53	e2 38856	. . . 4 |- (. -. E. x -. th ,. -. ch ->. E. x -. ps ).
55		hbe1 2021	. . . 4 |- ( E. x -. ps -> A. x E. x -. ps )
56	30, 54, 24, 55	exinst11 38851	. . 3 |- (. -. E. x -. th ->. E. x -. ps ).
57		exnal 1754	. . . 4 |- ( E. x -. ps <-> -. A. x ps )
58	57	biimpi 206	. . 3 |- ( E. x -. ps -> -. A. x ps )
59	56, 58	e1a 38852	. 2 |- (. -. E. x -. th ->. -. A. x ps ).
60	59	in1 38787	1 |- ( -. E. x -. th -> -. A. x ps )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-vd1 38786  df-vd2 38794

This theorem is referenced by: (None)