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

Theorem nic-mp 1636
 Description: Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply 𝜒, this form is necessary for useful derivations from nic-ax 1638. 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 𝜑
nic-jmaj (𝜑 ⊼ (𝜒𝜓))
Assertion
Ref Expression
nic-mp 𝜓

Proof of Theorem nic-mp
StepHypRef Expression
1 nic-jmin . 2 𝜑
2 nic-jmaj . . . 4 (𝜑 ⊼ (𝜒𝜓))
3 nannan 1491 . . . 4 ((𝜑 ⊼ (𝜒𝜓)) ↔ (𝜑 → (𝜒𝜓)))
42, 3mpbi 220 . . 3 (𝜑 → (𝜒𝜓))
54simprd 478 . 2 (𝜑𝜓)
61, 5ax-mp 5 1 𝜓
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ⊼ wnan 1487 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 197  df-an 385  df-nan 1488 This theorem is referenced by:  nic-imp  1640  nic-idlem2  1642  nic-id  1643  nic-swap  1644  nic-isw1  1645  nic-isw2  1646  nic-iimp1  1647  nic-idel  1649  nic-ich  1650  nic-stdmp  1655  nic-luk1  1656  nic-luk2  1657  nic-luk3  1658  lukshefth1  1660  lukshefth2  1661  renicax  1662
 Copyright terms: Public domain W3C validator