Theorem nic-dfim

This theorem "defines" implication in terms of 'nand'. Analogous to nanim. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion

$ \vdash ((\varphi \barwedge (\psi \barwedge \psi)) \barwedge (\varphi \rightarrow \psi)) \barwedge (((\varphi \barwedge (\psi \barwedge \psi)) \barwedge (\varphi \barwedge (\psi \barwedge \psi))) \barwedge ((\varphi \rightarrow \psi) \barwedge (\varphi \rightarrow \psi))) $

Proof

nanim

bicomi _

$ \vdash \varphi \barwedge (\psi \barwedge \psi) \leftrightarrow \varphi \rightarrow \psi $

nanbi

$ \vdash \varphi \barwedge (\psi \barwedge \psi) \leftrightarrow \varphi \rightarrow \psi \leftrightarrow ((\varphi \barwedge (\psi \barwedge \psi)) \barwedge (\varphi \rightarrow \psi)) \barwedge (((\varphi \barwedge (\psi \barwedge \psi)) \barwedge (\varphi \barwedge (\psi \barwedge \psi))) \barwedge ((\varphi \rightarrow \psi) \barwedge (\varphi \rightarrow \psi))) $

mpbi l1 _