MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nic-ax Structured version   Unicode version

Theorem nic-ax 1481
Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1447, the usual axioms can be derived from this and vice versa. Unlike meredith 1447, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g.  { nic-ax 1481, nic-mp 1479 
} is equivalent to  { luk-1 1463, luk-2 1464, luk-3 1465, ax-mp 5  }. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
nic-ax  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  -/\  (
( ta  -/\  ( ta  -/\  ta ) ) 
-/\  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) )

Proof of Theorem nic-ax
StepHypRef Expression
1 nannan 1338 . . . . 5  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  <->  ( ph  ->  ( ch  /\  ps ) ) )
21biimpi 194 . . . 4  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  ->  ( ph  ->  ( ch  /\  ps ) ) )
3 simpl 457 . . . . 5  |-  ( ( ch  /\  ps )  ->  ch )
43imim2i 14 . . . 4  |-  ( (
ph  ->  ( ch  /\  ps ) )  ->  ( ph  ->  ch ) )
5 imnan 422 . . . . . . 7  |-  ( ( th  ->  -.  ch )  <->  -.  ( th  /\  ch ) )
6 df-nan 1335 . . . . . . 7  |-  ( ( th  -/\  ch )  <->  -.  ( th  /\  ch ) )
75, 6bitr4i 252 . . . . . 6  |-  ( ( th  ->  -.  ch )  <->  ( th  -/\  ch )
)
8 con3 134 . . . . . . . 8  |-  ( (
ph  ->  ch )  -> 
( -.  ch  ->  -. 
ph ) )
98imim2d 52 . . . . . . 7  |-  ( (
ph  ->  ch )  -> 
( ( th  ->  -. 
ch )  ->  ( th  ->  -.  ph ) ) )
10 imnan 422 . . . . . . . 8  |-  ( (
ph  ->  -.  th )  <->  -.  ( ph  /\  th ) )
11 con2b 334 . . . . . . . 8  |-  ( ( th  ->  -.  ph )  <->  (
ph  ->  -.  th )
)
12 df-nan 1335 . . . . . . . 8  |-  ( (
ph  -/\  th )  <->  -.  ( ph  /\  th ) )
1310, 11, 123bitr4ri 278 . . . . . . 7  |-  ( (
ph  -/\  th )  <->  ( th  ->  -.  ph ) )
149, 13syl6ibr 227 . . . . . 6  |-  ( (
ph  ->  ch )  -> 
( ( th  ->  -. 
ch )  ->  ( ph  -/\  th ) ) )
157, 14syl5bir 218 . . . . 5  |-  ( (
ph  ->  ch )  -> 
( ( th  -/\  ch )  ->  ( ph  -/\  th )
) )
16 nanim 1339 . . . . 5  |-  ( ( ( th  -/\  ch )  ->  ( ph  -/\  th )
)  <->  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) )
1715, 16sylib 196 . . . 4  |-  ( (
ph  ->  ch )  -> 
( ( th  -/\  ch )  -/\  ( ( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) )
182, 4, 173syl 20 . . 3  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  ->  (
( th  -/\  ch )  -/\  ( ( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) )
19 pm4.24 643 . . . . 5  |-  ( ta  <->  ( ta  /\  ta )
)
2019biimpi 194 . . . 4  |-  ( ta 
->  ( ta  /\  ta ) )
21 nannan 1338 . . . 4  |-  ( ( ta  -/\  ( ta  -/\ 
ta ) )  <->  ( ta  ->  ( ta  /\  ta ) ) )
2220, 21mpbir 209 . . 3  |-  ( ta 
-/\  ( ta  -/\  ta ) )
2318, 22jctil 537 . 2  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  ->  (
( ta  -/\  ( ta  -/\  ta ) )  /\  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) )
24 nannan 1338 . 2  |-  ( ( ( ph  -/\  ( ch  -/\  ps ) ) 
-/\  ( ( ta 
-/\  ( ta  -/\  ta ) )  -/\  (
( th  -/\  ch )  -/\  ( ( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) )  <-> 
( ( ph  -/\  ( ch  -/\  ps ) )  ->  ( ( ta 
-/\  ( ta  -/\  ta ) )  /\  (
( th  -/\  ch )  -/\  ( ( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) ) )
2523, 24mpbir 209 1  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  -/\  (
( ta  -/\  ( ta  -/\  ta ) ) 
-/\  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    -/\ wnan 1334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-nan 1335
This theorem is referenced by:  nic-imp  1483  nic-idlem1  1484  nic-idlem2  1485  nic-id  1486  nic-swap  1487  nic-luk1  1499  lukshef-ax1  1502
  Copyright terms: Public domain W3C validator