Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  vk15.4j Structured version   Unicode version

Theorem vk15.4j 36555
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 36555 is vk15.4jVD 36984 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
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
Ref Expression
vk15.4j  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )

Proof of Theorem vk15.4j
StepHypRef Expression
1 vk15.4j.3 . . . . . 6  |-  -.  A. x ( ta  ->  ph )
2 exanali 1715 . . . . . 6  |-  ( E. x ( ta  /\  -.  ph )  <->  -.  A. x
( ta  ->  ph )
)
31, 2mpbir 212 . . . . 5  |-  E. x
( ta  /\  -.  ph )
4 vk15.4j.2 . . . . . 6  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta ) )
5 alex 1694 . . . . . . . . . 10  |-  ( A. x th  <->  -.  E. x  -.  th )
65biimpri 209 . . . . . . . . 9  |-  ( -. 
E. x  -.  th  ->  A. x th )
7619.21bi 1919 . . . . . . . 8  |-  ( -. 
E. x  -.  th  ->  th )
8 simpl 458 . . . . . . . . 9  |-  ( ( ta  /\  -.  ph )  ->  ta )
98a1i 11 . . . . . . . 8  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  ta ) )
10 19.8a 1907 . . . . . . . 8  |-  ( ( th  /\  ta )  ->  E. x ( th 
/\  ta ) )
117, 9, 10syl6an 547 . . . . . . 7  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  E. x
( th  /\  ta ) ) )
12 notnot1 125 . . . . . . 7  |-  ( E. x ( th  /\  ta )  ->  -.  -.  E. x ( th  /\  ta ) )
1311, 12syl6 34 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  -.  -.  E. x ( th 
/\  ta ) ) )
14 con3 139 . . . . . 6  |-  ( ( A. x ch  ->  -. 
E. x ( th 
/\  ta ) )  -> 
( -.  -.  E. x ( th  /\  ta )  ->  -.  A. x ch ) )
154, 13, 14ee02 36506 . . . . 5  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  -.  A. x ch ) )
16 hbe1 1888 . . . . . 6  |-  ( E. x  -.  th  ->  A. x E. x  -.  th )
1716hbn 1949 . . . . 5  |-  ( -. 
E. x  -.  th  ->  A. x  -.  E. x  -.  th )
18 hbn1 1887 . . . . 5  |-  ( -. 
A. x ch  ->  A. x  -.  A. x ch )
193, 15, 17, 18eexinst01 36553 . . . 4  |-  ( -. 
E. x  -.  th  ->  -.  A. x ch )
20 exnal 1695 . . . 4  |-  ( E. x  -.  ch  <->  -.  A. x ch )
2119, 20sylibr 215 . . 3  |-  ( -. 
E. x  -.  th  ->  E. x  -.  ch )
22 vk15.4j.1 . . . . . . . . 9  |-  -.  ( E. x  -.  ph  /\  E. x ( ps  /\  -.  ch ) )
23 pm3.13 503 . . . . . . . . 9  |-  ( -.  ( E. x  -.  ph 
/\  E. x ( ps 
/\  -.  ch )
)  ->  ( -.  E. x  -.  ph  \/  -.  E. x ( ps 
/\  -.  ch )
) )
2422, 23ax-mp 5 . . . . . . . 8  |-  ( -. 
E. x  -.  ph  \/  -.  E. x ( ps  /\  -.  ch ) )
25 simpr 462 . . . . . . . . . . . 12  |-  ( ( ta  /\  -.  ph )  ->  -.  ph )
2625a1i 11 . . . . . . . . . . 11  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  -.  ph ) )
27 19.8a 1907 . . . . . . . . . . 11  |-  ( -. 
ph  ->  E. x  -.  ph )
2826, 27syl6 34 . . . . . . . . . 10  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  E. x  -.  ph ) )
29 hbe1 1888 . . . . . . . . . 10  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
303, 28, 17, 29eexinst01 36553 . . . . . . . . 9  |-  ( -. 
E. x  -.  th  ->  E. x  -.  ph )
31 notnot1 125 . . . . . . . . 9  |-  ( E. x  -.  ph  ->  -. 
-.  E. x  -.  ph )
3230, 31syl 17 . . . . . . . 8  |-  ( -. 
E. x  -.  th  ->  -.  -.  E. x  -.  ph )
33 pm2.53 374 . . . . . . . 8  |-  ( ( -.  E. x  -.  ph  \/  -.  E. x
( ps  /\  -.  ch ) )  ->  ( -.  -.  E. x  -.  ph 
->  -.  E. x ( ps  /\  -.  ch ) ) )
3424, 32, 33mpsyl 65 . . . . . . 7  |-  ( -. 
E. x  -.  th  ->  -.  E. x ( ps  /\  -.  ch ) )
35 exanali 1715 . . . . . . . 8  |-  ( E. x ( ps  /\  -.  ch )  <->  -.  A. x
( ps  ->  ch ) )
3635con5i 36550 . . . . . . 7  |-  ( -. 
E. x ( ps 
/\  -.  ch )  ->  A. x ( ps 
->  ch ) )
3734, 36syl 17 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  A. x ( ps 
->  ch ) )
383719.21bi 1919 . . . . 5  |-  ( -. 
E. x  -.  th  ->  ( ps  ->  ch ) )
3938con3d 138 . . . 4  |-  ( -. 
E. x  -.  th  ->  ( -.  ch  ->  -. 
ps ) )
40 19.8a 1907 . . . 4  |-  ( -. 
ps  ->  E. x  -.  ps )
4139, 40syl6 34 . . 3  |-  ( -. 
E. x  -.  th  ->  ( -.  ch  ->  E. x  -.  ps )
)
42 hbe1 1888 . . 3  |-  ( E. x  -.  ps  ->  A. x E. x  -.  ps )
4321, 41, 17, 42eexinst11 36554 . 2  |-  ( -. 
E. x  -.  th  ->  E. x  -.  ps )
44 exnal 1695 . 2  |-  ( E. x  -.  ps  <->  -.  A. x ps )
4543, 44sylib 199 1  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369    /\ wa 370   A.wal 1435   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-12 1904
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator