New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nic-mp GIF version

Theorem nic-mp 1436
 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 1438. 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 1291 . . . 4 ((φ (χ ψ)) ↔ (φ → (χ ψ)))
42, 3mpbi 199 . . 3 (φ → (χ ψ))
54simprd 449 . 2 (φψ)
61, 5ax-mp 8 1 ψ
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ⊼ wnan 1287 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 This theorem is referenced by:  nic-imp  1440  nic-idlem2  1442  nic-id  1443  nic-swap  1444  nic-isw1  1445  nic-isw2  1446  nic-iimp1  1447  nic-idel  1449  nic-ich  1450  nic-stdmp  1455  nic-luk1  1456  nic-luk2  1457  nic-luk3  1458  lukshefth1  1460  lukshefth2  1461  renicax  1462
 Copyright terms: Public domain W3C validator