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

Theorem nic-mp 1445
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 1447. 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 1300 . . . 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 1296
This theorem is referenced by:  nic-imp  1449  nic-idlem2  1451  nic-id  1452  nic-swap  1453  nic-isw1  1454  nic-isw2  1455  nic-iimp1  1456  nic-idel  1458  nic-ich  1459  nic-stdmp  1464  nic-luk1  1465  nic-luk2  1466  nic-luk3  1467  lukshefth1  1469  lukshefth2  1470  renicax  1471
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 1297
  Copyright terms: Public domain W3C validator