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

Theorem nic-mp 1548
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 1550. 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 1384 . . . 4  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  <->  ( ph  ->  ( ch  /\  ps ) ) )
42, 3mpbi 211 . . 3  |-  ( ph  ->  ( ch  /\  ps ) )
54simprd 464 . 2  |-  ( ph  ->  ps )
61, 5ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> 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-idlem2  1554  nic-id  1555  nic-swap  1556  nic-isw1  1557  nic-isw2  1558  nic-iimp1  1559  nic-idel  1561  nic-ich  1562  nic-stdmp  1567  nic-luk1  1568  nic-luk2  1569  nic-luk3  1570  lukshefth1  1572  lukshefth2  1573  renicax  1574
  Copyright terms: Public domain W3C validator