Theorem nic-mp 1701

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 1703. 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

Step	Hyp	Ref	Expression
1		nic-jmin	. 2 ⊢ 𝜑
2		nic-jmaj	. . . 4 ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))
3		nannan 1527	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
4	2, 3	mpbi 233	. . 3 ⊢ (𝜑 → (𝜒 ∧ 𝜓))
5	4	simprd 500	. 2 ⊢ (𝜑 → 𝜓)
6	1, 5	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4   ∧ wa 400   ⊼ wnan 1521

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 210  df-an 401  df-nan 1522

This theorem is referenced by:  nic-imp  1705  nic-idlem2  1707  nic-id  1708  nic-swap  1709  nic-isw1  1710  nic-isw2  1711  nic-iimp1  1712  nic-idel  1714  nic-ich  1715  nic-stdmp  1720  nic-luk1  1721  nic-luk2  1722  nic-luk3  1723  lukshefth1  1725  lukshefth2  1726  renicax  1727