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 32254
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 32254 is vk15.4jVD 32671 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 1642 . . . . . 6  |-  ( E. x ( ta  /\  -.  ph )  <->  -.  A. x
( ta  ->  ph )
)
31, 2mpbir 209 . . . . 5  |-  E. x
( ta  /\  -.  ph )
4 vk15.4j.2 . . . . . 6  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta ) )
5 alex 1622 . . . . . . . . . 10  |-  ( A. x th  <->  -.  E. x  -.  th )
65biimpri 206 . . . . . . . . 9  |-  ( -. 
E. x  -.  th  ->  A. x th )
7619.21bi 1813 . . . . . . . 8  |-  ( -. 
E. x  -.  th  ->  th )
8 simpl 457 . . . . . . . . 9  |-  ( ( ta  /\  -.  ph )  ->  ta )
98a1i 11 . . . . . . . 8  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  ta ) )
10 19.8a 1801 . . . . . . . 8  |-  ( ( th  /\  ta )  ->  E. x ( th 
/\  ta ) )
117, 9, 10syl6an 545 . . . . . . 7  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  E. x
( th  /\  ta ) ) )
12 notnot1 122 . . . . . . 7  |-  ( E. x ( th  /\  ta )  ->  -.  -.  E. x ( th  /\  ta ) )
1311, 12syl6 33 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  -.  -.  E. x ( th 
/\  ta ) ) )
14 con3 134 . . . . . 6  |-  ( ( A. x ch  ->  -. 
E. x ( th 
/\  ta ) )  -> 
( -.  -.  E. x ( th  /\  ta )  ->  -.  A. x ch ) )
154, 13, 14ee02 32179 . . . . 5  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  -.  A. x ch ) )
16 hbe1 1783 . . . . . 6  |-  ( E. x  -.  th  ->  A. x E. x  -.  th )
1716hbn 1838 . . . . 5  |-  ( -. 
E. x  -.  th  ->  A. x  -.  E. x  -.  th )
18 hbn1 1782 . . . . 5  |-  ( -. 
A. x ch  ->  A. x  -.  A. x ch )
193, 15, 17, 18eexinst01 32252 . . . 4  |-  ( -. 
E. x  -.  th  ->  -.  A. x ch )
20 exnal 1623 . . . 4  |-  ( E. x  -.  ch  <->  -.  A. x ch )
2119, 20sylibr 212 . . 3  |-  ( -. 
E. x  -.  th  ->  E. x  -.  ch )
22 vk15.4j.1 . . . . . . . . 9  |-  -.  ( E. x  -.  ph  /\  E. x ( ps  /\  -.  ch ) )
23 pm3.13 501 . . . . . . . . 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 461 . . . . . . . . . . . 12  |-  ( ( ta  /\  -.  ph )  ->  -.  ph )
2625a1i 11 . . . . . . . . . . 11  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  -.  ph ) )
27 19.8a 1801 . . . . . . . . . . 11  |-  ( -. 
ph  ->  E. x  -.  ph )
2826, 27syl6 33 . . . . . . . . . 10  |-  ( -. 
E. x  -.  th  ->  ( ( ta  /\  -.  ph )  ->  E. x  -.  ph ) )
29 hbe1 1783 . . . . . . . . . 10  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
303, 28, 17, 29eexinst01 32252 . . . . . . . . 9  |-  ( -. 
E. x  -.  th  ->  E. x  -.  ph )
31 notnot1 122 . . . . . . . . 9  |-  ( E. x  -.  ph  ->  -. 
-.  E. x  -.  ph )
3230, 31syl 16 . . . . . . . 8  |-  ( -. 
E. x  -.  th  ->  -.  -.  E. x  -.  ph )
33 pm2.53 373 . . . . . . . 8  |-  ( ( -.  E. x  -.  ph  \/  -.  E. x
( ps  /\  -.  ch ) )  ->  ( -.  -.  E. x  -.  ph 
->  -.  E. x ( ps  /\  -.  ch ) ) )
3424, 32, 33mpsyl 63 . . . . . . 7  |-  ( -. 
E. x  -.  th  ->  -.  E. x ( ps  /\  -.  ch ) )
35 exanali 1642 . . . . . . . 8  |-  ( E. x ( ps  /\  -.  ch )  <->  -.  A. x
( ps  ->  ch ) )
3635con5i 32249 . . . . . . 7  |-  ( -. 
E. x ( ps 
/\  -.  ch )  ->  A. x ( ps 
->  ch ) )
3734, 36syl 16 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  A. x ( ps 
->  ch ) )
383719.21bi 1813 . . . . 5  |-  ( -. 
E. x  -.  th  ->  ( ps  ->  ch ) )
3938con3d 133 . . . 4  |-  ( -. 
E. x  -.  th  ->  ( -.  ch  ->  -. 
ps ) )
40 19.8a 1801 . . . 4  |-  ( -. 
ps  ->  E. x  -.  ps )
4139, 40syl6 33 . . 3  |-  ( -. 
E. x  -.  th  ->  ( -.  ch  ->  E. x  -.  ps )
)
42 hbe1 1783 . . 3  |-  ( E. x  -.  ps  ->  A. x E. x  -.  ps )
4321, 41, 17, 42eexinst11 32253 . 2  |-  ( -. 
E. x  -.  th  ->  E. x  -.  ps )
44 exnal 1623 . 2  |-  ( E. x  -.  ps  <->  -.  A. x ps )
4543, 44sylib 196 1  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368    /\ wa 369   A.wal 1372   E.wex 1591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator