Theorem nic-mp 1596

Description: Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply ch, this form is necessary for useful derivations from nic-ax 1598. 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	|- ph
nic-jmaj	|- ( ph -/\ ( ch -/\ ps ) )

Assertion

Ref	Expression
nic-mp	|- ps

Proof of Theorem nic-mp

Step	Hyp	Ref	Expression
1		nic-jmin	. 2 |- ph
2		nic-jmaj	. . . 4 |- ( ph -/\ ( ch -/\ ps ) )
3		nannan 1451	. . . 4 |- ( ( ph -/\ ( ch -/\ ps ) ) <-> ( ph -> ( ch /\ ps ) ) )
4	2, 3	mpbi 220	. . 3 |- ( ph -> ( ch /\ ps ) )
5	4	simprd 479	. 2 |- ( ph -> ps )
6	1, 5	ax-mp 5	1 |- ps

Syntax hints:   -> wi 4   /\ wa 384   -/\ wnan 1447

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 386  df-nan 1448

This theorem is referenced by:  nic-imp  1600  nic-idlem2  1602  nic-id  1603  nic-swap  1604  nic-isw1  1605  nic-isw2  1606  nic-iimp1  1607  nic-idel  1609  nic-ich  1610  nic-stdmp  1615  nic-luk1  1616  nic-luk2  1617  nic-luk3  1618  lukshefth1  1620  lukshefth2  1621  renicax  1622