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

Theorem nic-mp 1426
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 1428. 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 1291 . . . 4  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  <->  ( ph  ->  ( ch  /\  ps ) ) )
42, 3mpbi 199 . . 3  |-  ( ph  ->  ( ch  /\  ps ) )
54simprd 449 . 2  |-  ( ph  ->  ps )
61, 5ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    -/\ wnan 1287
This theorem is referenced by:  nic-imp  1430  nic-idlem2  1432  nic-id  1433  nic-swap  1434  nic-isw1  1435  nic-isw2  1436  nic-iimp1  1437  nic-idel  1439  nic-ich  1440  nic-stdmp  1445  nic-luk1  1446  nic-luk2  1447  nic-luk3  1448  lukshefth1  1450  lukshefth2  1451  renicax  1452
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 177  df-an 360  df-nan 1288
  Copyright terms: Public domain W3C validator