Theorem nic-mp 1745

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 1747. 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 1600	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
4	2, 3	mpbi 220	. . 3 ⊢ (𝜑 → (𝜒 ∧ 𝜓))
5	4	simprd 482	. 2 ⊢ (𝜑 → 𝜓)
6	1, 5	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4   ∧ wa 383   ⊼ wnan 1596

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 1597

This theorem is referenced by:  nic-imp  1749  nic-idlem2  1751  nic-id  1752  nic-swap  1753  nic-isw1  1754  nic-isw2  1755  nic-iimp1  1756  nic-idel  1758  nic-ich  1759  nic-stdmp  1764  nic-luk1  1765  nic-luk2  1766  nic-luk3  1767  lukshefth1  1769  lukshefth2  1770  renicax  1771