Theorem nic-mp 1703

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 1705. 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 1526	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
4	2, 3	mpbi 233	. . 3 ⊢ (𝜑 → (𝜒 ∧ 𝜓))
5	4	simprd 501	. 2 ⊢ (𝜑 → 𝜓)
6	1, 5	ax-mp 5	1 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊼ wnan 1520

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-nan 1521

This theorem is used by:  nic-imp  1707  nic-idlem2  1709  nic-id  1710  nic-swap  1711  nic-isw1  1712  nic-isw2  1713  nic-iimp1  1714  nic-idel  1716  nic-ich  1717  nic-stdmp  1722  nic-luk1  1723  nic-luk2  1724  nic-luk3  1725  lukshefth1  1727  lukshefth2  1728  renicax  1729