Theorem nic-mp 1669

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 1671. 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 1494	. . . 4 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓)))
4	2, 3	mpbi 230	. . 3 ⊢ (𝜑 → (𝜒 ∧ 𝜓))
5	4	simprd 495	. 2 ⊢ (𝜑 → 𝜓)
6	1, 5	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4   ∧ wa 395   ⊼ wnan 1488

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 207  df-an 396  df-nan 1489

This theorem is referenced by:  nic-imp  1673  nic-idlem2  1675  nic-id  1676  nic-swap  1677  nic-isw1  1678  nic-isw2  1679  nic-iimp1  1680  nic-idel  1682  nic-ich  1683  nic-stdmp  1688  nic-luk1  1689  nic-luk2  1690  nic-luk3  1691  lukshefth1  1693  lukshefth2  1694  renicax  1695