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 φ χ ψ τ τ τ θ χ φ θ φ θ

Proof

Step Hyp Ref Expression
1 nannan φ χ ψ φ χ ψ
2 1 biimpi φ χ ψ φ χ ψ
3 simpl χ ψ χ
4 3 imim2i φ χ ψ φ χ
5 imnan θ ¬ χ ¬ θ χ
6 df-nan θ χ ¬ θ χ
7 5 6 bitr4i θ ¬ χ θ χ
8 con3 φ χ ¬ χ ¬ φ
9 8 imim2d φ χ θ ¬ χ θ ¬ φ
10 imnan φ ¬ θ ¬ φ θ
11 con2b θ ¬ φ φ ¬ θ
12 df-nan φ θ ¬ φ θ
13 10 11 12 3bitr4ri φ θ θ ¬ φ
14 9 13 syl6ibr φ χ θ ¬ χ φ θ
15 7 14 syl5bir φ χ θ χ φ θ
16 nanim θ χ φ θ θ χ φ θ φ θ
17 15 16 sylib φ χ θ χ φ θ φ θ
18 2 4 17 3syl φ χ ψ θ χ φ θ φ θ
19 pm4.24 τ τ τ
20 19 biimpi τ τ τ
21 nannan τ τ τ τ τ τ
22 20 21 mpbir τ τ τ
23 18 22 jctil φ χ ψ τ τ τ θ χ φ θ φ θ
24 nannan φ χ ψ τ τ τ θ χ φ θ φ θ φ χ ψ τ τ τ θ χ φ θ φ θ
25 23 24 mpbir φ χ ψ τ τ τ θ χ φ θ φ θ