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

Theorem nic-mp 1442
Description: Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply  ch, this form is necessary for useful derivations from nic-ax 1444. 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.)
Hypotheses
Ref Expression
nic-jmin  |-  ph
nic-jmaj  |-  ( ph  -/\  ( ch  -/\  ps )
)
Assertion
Ref Expression
nic-mp  |-  ps

Proof of Theorem nic-mp
StepHypRef Expression
1 nic-jmin . 2  |-  ph
2 nic-jmaj . . . 4  |-  ( ph  -/\  ( ch  -/\  ps )
)
3 nannan 1297 . . . 4  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  <->  ( ph  ->  ( ch  /\  ps ) ) )
42, 3mpbi 200 . . 3  |-  ( ph  ->  ( ch  /\  ps ) )
54simprd 450 . 2  |-  ( ph  ->  ps )
61, 5ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    -/\ wnan 1293
This theorem is referenced by:  nic-imp  1446  nic-idlem2  1448  nic-id  1449  nic-swap  1450  nic-isw1  1451  nic-isw2  1452  nic-iimp1  1453  nic-idel  1455  nic-ich  1456  nic-stdmp  1461  nic-luk1  1462  nic-luk2  1463  nic-luk3  1464  lukshefth1  1466  lukshefth2  1467  renicax  1468
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-nan 1294
  Copyright terms: Public domain W3C validator