Theorem nic-mp 1666

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 1668. 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 1491	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
4	2, 3	mpbi 229	. . 3 ⊢ (𝜑 → (𝜒 ∧ 𝜓))
5	4	simprd 494	. 2 ⊢ (𝜑 → 𝜓)
6	1, 5	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4   ∧ wa 394   ⊼ wnan 1485

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 206  df-an 395  df-nan 1486

This theorem is referenced by:  nic-imp  1670  nic-idlem2  1672  nic-id  1673  nic-swap  1674  nic-isw1  1675  nic-isw2  1676  nic-iimp1  1677  nic-idel  1679  nic-ich  1680  nic-stdmp  1685  nic-luk1  1686  nic-luk2  1687  nic-luk3  1688  lukshefth1  1690  lukshefth2  1691  renicax  1692