Theorem nic-mp 1084

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 1086. 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.)

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		nic-justlem 1078	. . . 4 |- ((ph -/\ (ch -/\ ps)) <-> (ph -> (ch /\ ps)))
4	2, 3	mpbi 205	. . 3 |- (ph -> (ch /\ ps))
5	4	pm3.27d 350	. 2 |- (ph -> ps)
6	1, 5	ax-mp 7	1 |- ps

Syntax hints:   -> wi 3   /\ wa 239   -/\ wnand 1076

This theorem is referenced by:  nic-imp 1088  nic-idlem2 1090  nic-id 1091  nic-swap 1092  nic-isw1 1093  nic-isw2 1094  nic-iimp1 1095  nic-idel 1097  nic-ich 1098  nic-stdmp 1103  nic-luk1 1104  nic-luk2 1105  nic-luk3 1106  lukshefth1 13892  lukshefth2 13893  renicax 13894

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 163  df-an 241  df-nand 1077

Copyright terms: Public domain