Theorem nic-ax
Nicod's axiom derived from the standard ones. See Introduction to
Mathematical Philosophy by B. Russell, p. 152. Like meredith, the
usual axioms can be derived from this and vice versa. Unlike meredith,
Nicod uses a different connective ('nand'), so another form of modus
ponens must be used in proofs, e.g., { nic-ax, nic-mp } is
equivalent to { luk-1, luk-2, luk-3, [ax-mp] }. 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.)
Conclusion
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \)
Proof
nannan
l1
biimpi _
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \rightarrow \varphi \rightarrow \chi \wedge \psi \)
simpl
l3
imim2i _
\( \vdash (\varphi \rightarrow \chi \wedge \psi) \rightarrow \varphi \rightarrow \chi \)
l4
imnan
\( \vdash \theta \rightarrow \neg \chi \leftrightarrow \neg (\theta \wedge \chi) \)
df-nan
\( \vdash \theta \barwedge \chi \leftrightarrow \neg (\theta \wedge \chi) \)
l6
bitr4i l4 _
\( \vdash \theta \rightarrow \neg \chi \leftrightarrow \theta \barwedge \chi \)
con3
l8
imim2d _
\( \vdash (\varphi \rightarrow \chi) \rightarrow (\theta \rightarrow \neg \chi) \rightarrow \theta \rightarrow \neg \varphi \)
l9
imnan
\( \vdash \varphi \rightarrow \neg \theta \leftrightarrow \neg (\varphi \wedge \theta) \)
l10
con2b
\( \vdash \theta \rightarrow \neg \varphi \leftrightarrow \varphi \rightarrow \neg \theta \)
df-nan
\( \vdash \varphi \barwedge \theta \leftrightarrow \neg (\varphi \wedge \theta) \)
3bitr4ri l9 l10 _
\( \vdash \varphi \barwedge \theta \leftrightarrow \theta \rightarrow \neg \varphi \)
imbitrrdi l8 _
\( \vdash (\varphi \rightarrow \chi) \rightarrow (\theta \rightarrow \neg \chi) \rightarrow \varphi \barwedge \theta \)
l14
biimtrrid l6 _
\( \vdash (\varphi \rightarrow \chi) \rightarrow \theta \barwedge \chi \rightarrow \varphi \barwedge \theta \)
nanim
\( \vdash \theta \barwedge \chi \rightarrow \varphi \barwedge \theta \leftrightarrow (\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)) \)
sylib l14 _
\( \vdash (\varphi \rightarrow \chi) \rightarrow (\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)) \)
l17
3syl l1 l3 _
pm4.24
l19
biimpi _
\( \vdash \tau \rightarrow \tau \wedge \tau \)
nannan
\( \vdash \tau \barwedge (\tau \barwedge \tau) \leftrightarrow \tau \rightarrow \tau \wedge \tau \)
mpbir l19 _
l22
jctil l17 _
\( \vdash \varphi \barwedge (\chi \barwedge \psi) \rightarrow (\tau \barwedge (\tau \barwedge \tau)) \wedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \)
nannan
\( \vdash (\varphi \barwedge (\chi \barwedge \psi)) \barwedge ((\tau \barwedge (\tau \barwedge \tau)) \barwedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta)))) \leftrightarrow \varphi \barwedge (\chi \barwedge \psi) \rightarrow (\tau \barwedge (\tau \barwedge \tau)) \wedge ((\theta \barwedge \chi) \barwedge ((\varphi \barwedge \theta) \barwedge (\varphi \barwedge \theta))) \)
mpbir l22 _