Theorem waj-ax 37172

Description: A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011.)

Assertion

Ref	Expression
waj-ax	⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜑 ⊼ 𝜓))))

Proof of Theorem waj-ax

Step	Hyp	Ref	Expression
1		nannan 1527	. . 3 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
2		simpr 490	. . . . . . . . 9 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
3	2	imim2i 17	. . . . . . . 8 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒))
4		pm2.27 43	. . . . . . . . . 10 ⊢ (𝜑 → ((𝜑 → 𝜒) → 𝜒))
5	4	anim2d 624	. . . . . . . . 9 ⊢ (𝜑 → ((𝜃 ∧ (𝜑 → 𝜒)) → (𝜃 ∧ 𝜒)))
6	5	expdimp 458	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜃) → ((𝜑 → 𝜒) → (𝜃 ∧ 𝜒)))
7	3, 6	syl5com 32	. . . . . . 7 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜒)))
8	7	con3d 153	. . . . . 6 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (¬ (𝜃 ∧ 𝜒) → ¬ (𝜑 ∧ 𝜃)))
9		df-nan 1522	. . . . . 6 ⊢ ((𝜃 ⊼ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
10		df-nan 1522	. . . . . 6 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
11	8, 9, 10	3imtr4g 299	. . . . 5 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)))
12		nanim 1528	. . . . 5 ⊢ (((𝜃 ⊼ 𝜒) → (𝜑 ⊼ 𝜃)) ↔ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
13	11, 12	sylib 221	. . . 4 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
14		pm3.21 477	. . . . . . . 8 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
15	14	adantr 486	. . . . . . 7 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → (𝜑 ∧ 𝜓)))
16	15	com12 33	. . . . . 6 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)))
17	16	a2i 15	. . . . 5 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → (𝜑 ∧ 𝜓)))
18		nannan 1527	. . . . 5 ⊢ ((𝜑 ⊼ (𝜑 ⊼ 𝜓)) ↔ (𝜑 → (𝜑 ∧ 𝜓)))
19	17, 18	sylibr 237	. . . 4 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 ⊼ (𝜑 ⊼ 𝜓)))
20	13, 19	jca 521	. . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ∧ (𝜑 ⊼ (𝜑 ⊼ 𝜓))))
21	1, 20	sylbi 220	. 2 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ∧ (𝜑 ⊼ (𝜑 ⊼ 𝜓))))
22		nannan 1527	. 2 ⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜑 ⊼ 𝜓)))) ↔ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ∧ (𝜑 ⊼ (𝜑 ⊼ 𝜓)))))
23	21, 22	mpbir 234	1 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜑 ⊼ 𝜓))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ⊼ wnan 1521

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-nan 1522

This theorem is used by: (None)