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 imbitrrdi ⊢φ→χ→θ→¬χ→φ⊼θ
15 7 14 biimtrrid ⊢φ→χ→θ⊼χ→φ⊼θ
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 ⊢φ⊼χ⊼ψ⊼τ⊼τ⊼τ⊼θ⊼χ⊼φ⊼θ⊼φ⊼θ