Theorem nic-mp 1678

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 1680. 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 1504	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
4	2, 3	mpbi 231	. . 3 ⊢ (𝜑 → (𝜒 ∧ 𝜓))
5	4	simprd 496	. 2 ⊢ (𝜑 → 𝜓)
6	1, 5	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4   ∧ wa 396   ⊼ wnan 1498

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 208  df-an 397  df-nan 1499

This theorem is referenced by:  nic-imp  1682  nic-idlem2  1684  nic-id  1685  nic-swap  1686  nic-isw1  1687  nic-isw2  1688  nic-iimp1  1689  nic-idel  1691  nic-ich  1692  nic-stdmp  1697  nic-luk1  1698  nic-luk2  1699  nic-luk3  1700  lukshefth1  1702  lukshefth2  1703  renicax  1704