Theorem nic-ax 1438

Description: Nicod's axiom derived from the standard ones. See _Intro. to Math. Phil._ by B. Russell, p. 152. Like meredith 1404, the usual axioms can be derived from this and vice versa. Unlike meredith 1404, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1438, nic-mp 1436 } is equivalent to { luk-1 1420, luk-2 1421, luk-3 1422, ax-mp 8 }. 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.)

Assertion

Ref	Expression
nic-ax	⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))

Proof of Theorem nic-ax

Step	Hyp	Ref	Expression
1		nannan 1291	. . . . 5 ⊢ ((φ ⊼ (χ ⊼ ψ)) ↔ (φ → (χ ∧ ψ)))
2	1	biimpi 186	. . . 4 ⊢ ((φ ⊼ (χ ⊼ ψ)) → (φ → (χ ∧ ψ)))
3		simpl 443	. . . . 5 ⊢ ((χ ∧ ψ) → χ)
4	3	imim2i 13	. . . 4 ⊢ ((φ → (χ ∧ ψ)) → (φ → χ))
5		imnan 411	. . . . . . 7 ⊢ ((θ → ¬ χ) ↔ ¬ (θ ∧ χ))
6		df-nan 1288	. . . . . . 7 ⊢ ((θ ⊼ χ) ↔ ¬ (θ ∧ χ))
7	5, 6	bitr4i 243	. . . . . 6 ⊢ ((θ → ¬ χ) ↔ (θ ⊼ χ))
8		con3 126	. . . . . . . 8 ⊢ ((φ → χ) → (¬ χ → ¬ φ))
9	8	imim2d 48	. . . . . . 7 ⊢ ((φ → χ) → ((θ → ¬ χ) → (θ → ¬ φ)))
10		imnan 411	. . . . . . . 8 ⊢ ((φ → ¬ θ) ↔ ¬ (φ ∧ θ))
11		con2b 324	. . . . . . . 8 ⊢ ((θ → ¬ φ) ↔ (φ → ¬ θ))
12		df-nan 1288	. . . . . . . 8 ⊢ ((φ ⊼ θ) ↔ ¬ (φ ∧ θ))
13	10, 11, 12	3bitr4ri 269	. . . . . . 7 ⊢ ((φ ⊼ θ) ↔ (θ → ¬ φ))
14	9, 13	syl6ibr 218	. . . . . 6 ⊢ ((φ → χ) → ((θ → ¬ χ) → (φ ⊼ θ)))
15	7, 14	syl5bir 209	. . . . 5 ⊢ ((φ → χ) → ((θ ⊼ χ) → (φ ⊼ θ)))
16		nanim 1292	. . . . 5 ⊢ (((θ ⊼ χ) → (φ ⊼ θ)) ↔ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))
17	15, 16	sylib 188	. . . 4 ⊢ ((φ → χ) → ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))
18	2, 4, 17	3syl 18	. . 3 ⊢ ((φ ⊼ (χ ⊼ ψ)) → ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))
19		pm4.24 624	. . . . 5 ⊢ (τ ↔ (τ ∧ τ))
20	19	biimpi 186	. . . 4 ⊢ (τ → (τ ∧ τ))
21		nannan 1291	. . . 4 ⊢ ((τ ⊼ (τ ⊼ τ)) ↔ (τ → (τ ∧ τ)))
22	20, 21	mpbir 200	. . 3 ⊢ (τ ⊼ (τ ⊼ τ))
23	18, 22	jctil 523	. 2 ⊢ ((φ ⊼ (χ ⊼ ψ)) → ((τ ⊼ (τ ⊼ τ)) ∧ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))
24		nannan 1291	. 2 ⊢ (((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) ↔ ((φ ⊼ (χ ⊼ ψ)) → ((τ ⊼ (τ ⊼ τ)) ∧ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))))
25	23, 24	mpbir 200	1 ⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358   ⊼ wnan 1287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360  df-nan 1288

This theorem is referenced by:  nic-imp  1440  nic-idlem1  1441  nic-idlem2  1442  nic-id  1443  nic-swap  1444  nic-luk1  1456  lukshef-ax1  1459