# Metamath Proof Explorer

## Theorem nic-ax

Description: Nicod's axiom derived from the standard ones. SeeIntroduction 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.)

Ref Expression
Assertion nic-ax ${⊢}\left(\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)⊼\left(\left({\tau }⊼\left({\tau }⊼{\tau }\right)\right)⊼\left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 nannan ${⊢}\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)↔\left({\phi }\to \left({\chi }\wedge {\psi }\right)\right)$
2 1 biimpi ${⊢}\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)\to \left({\phi }\to \left({\chi }\wedge {\psi }\right)\right)$
3 simpl ${⊢}\left({\chi }\wedge {\psi }\right)\to {\chi }$
4 3 imim2i ${⊢}\left({\phi }\to \left({\chi }\wedge {\psi }\right)\right)\to \left({\phi }\to {\chi }\right)$
5 imnan ${⊢}\left({\theta }\to ¬{\chi }\right)↔¬\left({\theta }\wedge {\chi }\right)$
6 df-nan ${⊢}\left({\theta }⊼{\chi }\right)↔¬\left({\theta }\wedge {\chi }\right)$
7 5 6 bitr4i ${⊢}\left({\theta }\to ¬{\chi }\right)↔\left({\theta }⊼{\chi }\right)$
8 con3 ${⊢}\left({\phi }\to {\chi }\right)\to \left(¬{\chi }\to ¬{\phi }\right)$
9 8 imim2d ${⊢}\left({\phi }\to {\chi }\right)\to \left(\left({\theta }\to ¬{\chi }\right)\to \left({\theta }\to ¬{\phi }\right)\right)$
10 imnan ${⊢}\left({\phi }\to ¬{\theta }\right)↔¬\left({\phi }\wedge {\theta }\right)$
11 con2b ${⊢}\left({\theta }\to ¬{\phi }\right)↔\left({\phi }\to ¬{\theta }\right)$
12 df-nan ${⊢}\left({\phi }⊼{\theta }\right)↔¬\left({\phi }\wedge {\theta }\right)$
13 10 11 12 3bitr4ri ${⊢}\left({\phi }⊼{\theta }\right)↔\left({\theta }\to ¬{\phi }\right)$
14 9 13 syl6ibr ${⊢}\left({\phi }\to {\chi }\right)\to \left(\left({\theta }\to ¬{\chi }\right)\to \left({\phi }⊼{\theta }\right)\right)$
15 7 14 syl5bir ${⊢}\left({\phi }\to {\chi }\right)\to \left(\left({\theta }⊼{\chi }\right)\to \left({\phi }⊼{\theta }\right)\right)$
16 nanim ${⊢}\left(\left({\theta }⊼{\chi }\right)\to \left({\phi }⊼{\theta }\right)\right)↔\left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)$
17 15 16 sylib ${⊢}\left({\phi }\to {\chi }\right)\to \left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)$
18 2 4 17 3syl ${⊢}\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)\to \left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)$
19 pm4.24 ${⊢}{\tau }↔\left({\tau }\wedge {\tau }\right)$
20 19 biimpi ${⊢}{\tau }\to \left({\tau }\wedge {\tau }\right)$
21 nannan ${⊢}\left({\tau }⊼\left({\tau }⊼{\tau }\right)\right)↔\left({\tau }\to \left({\tau }\wedge {\tau }\right)\right)$
22 20 21 mpbir ${⊢}\left({\tau }⊼\left({\tau }⊼{\tau }\right)\right)$
23 18 22 jctil ${⊢}\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)\to \left(\left({\tau }⊼\left({\tau }⊼{\tau }\right)\right)\wedge \left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)\right)$
24 nannan ${⊢}\left(\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)⊼\left(\left({\tau }⊼\left({\tau }⊼{\tau }\right)\right)⊼\left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)\right)\right)↔\left(\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)\to \left(\left({\tau }⊼\left({\tau }⊼{\tau }\right)\right)\wedge \left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)\right)\right)$
25 23 24 mpbir ${⊢}\left(\left({\phi }⊼\left({\chi }⊼{\psi }\right)\right)⊼\left(\left({\tau }⊼\left({\tau }⊼{\tau }\right)\right)⊼\left(\left({\theta }⊼{\chi }\right)⊼\left(\left({\phi }⊼{\theta }\right)⊼\left({\phi }⊼{\theta }\right)\right)\right)\right)\right)$