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

Theorem nic-ax 1550
Description: Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1517, the usual axioms can be derived from this and vice versa. Unlike meredith 1517, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g.  { nic-ax 1550, nic-mp 1548 
} is equivalent to  { luk-1 1532, luk-2 1533, luk-3 1534, 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 1384 . . . . 5  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  <->  ( ph  ->  ( ch  /\  ps ) ) )
21biimpi 197 . . . 4  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  ->  ( ph  ->  ( ch  /\  ps ) ) )
3 simpl 458 . . . . 5  |-  ( ( ch  /\  ps )  ->  ch )
43imim2i 16 . . . 4  |-  ( (
ph  ->  ( ch  /\  ps ) )  ->  ( ph  ->  ch ) )
5 imnan 423 . . . . . . 7  |-  ( ( th  ->  -.  ch )  <->  -.  ( th  /\  ch ) )
6 df-nan 1380 . . . . . . 7  |-  ( ( th  -/\  ch )  <->  -.  ( th  /\  ch ) )
75, 6bitr4i 255 . . . . . 6  |-  ( ( th  ->  -.  ch )  <->  ( th  -/\  ch )
)
8 con3 139 . . . . . . . 8  |-  ( (
ph  ->  ch )  -> 
( -.  ch  ->  -. 
ph ) )
98imim2d 54 . . . . . . 7  |-  ( (
ph  ->  ch )  -> 
( ( th  ->  -. 
ch )  ->  ( th  ->  -.  ph ) ) )
10 imnan 423 . . . . . . . 8  |-  ( (
ph  ->  -.  th )  <->  -.  ( ph  /\  th ) )
11 con2b 335 . . . . . . . 8  |-  ( ( th  ->  -.  ph )  <->  (
ph  ->  -.  th )
)
12 df-nan 1380 . . . . . . . 8  |-  ( (
ph  -/\  th )  <->  -.  ( ph  /\  th ) )
1310, 11, 123bitr4ri 281 . . . . . . 7  |-  ( (
ph  -/\  th )  <->  ( th  ->  -.  ph ) )
149, 13syl6ibr 230 . . . . . 6  |-  ( (
ph  ->  ch )  -> 
( ( th  ->  -. 
ch )  ->  ( ph  -/\  th ) ) )
157, 14syl5bir 221 . . . . 5  |-  ( (
ph  ->  ch )  -> 
( ( th  -/\  ch )  ->  ( ph  -/\  th )
) )
16 nanim 1386 . . . . 5  |-  ( ( ( th  -/\  ch )  ->  ( ph  -/\  th )
)  <->  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) )
1715, 16sylib 199 . . . 4  |-  ( (
ph  ->  ch )  -> 
( ( th  -/\  ch )  -/\  ( ( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) )
182, 4, 173syl 18 . . 3  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  ->  (
( th  -/\  ch )  -/\  ( ( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) )
19 pm4.24 647 . . . . 5  |-  ( ta  <->  ( ta  /\  ta )
)
2019biimpi 197 . . . 4  |-  ( ta 
->  ( ta  /\  ta ) )
21 nannan 1384 . . . 4  |-  ( ( ta  -/\  ( ta  -/\ 
ta ) )  <->  ( ta  ->  ( ta  /\  ta ) ) )
2220, 21mpbir 212 . . 3  |-  ( ta 
-/\  ( ta  -/\  ta ) )
2318, 22jctil 539 . 2  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  ->  (
( ta  -/\  ( ta  -/\  ta ) )  /\  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) )
24 nannan 1384 . 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 212 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 370    -/\ wnan 1379
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 188  df-an 372  df-nan 1380
This theorem is referenced by:  nic-imp  1552  nic-idlem1  1553  nic-idlem2  1554  nic-id  1555  nic-swap  1556  nic-luk1  1568  lukshef-ax1  1571
  Copyright terms: Public domain W3C validator