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