Metamath Proof Explorer


Theorem nic-mp

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

Ref Expression
Hypotheses nic-jmin
|- ph
nic-jmaj
|- ( ph -/\ ( ch -/\ ps ) )
Assertion nic-mp
|- ps

Proof

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