Theorem lukshef-ax2 37125

Description: A single axiom for propositional calculus discovered by Jan Lukasiewicz. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom L2 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.)

Assertion

Ref	Expression
lukshef-ax2	⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

Proof of Theorem lukshef-ax2

Step	Hyp	Ref	Expression
1		nannan 1527	. . . 4 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
2	1	biimpi 219	. . 3 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒)))
3		simpr 490	. . . . 5 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
4	3	imim2i 17	. . . 4 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒))
5		simpl 488	. . . . . 6 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
6	5	imim2i 17	. . . . 5 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜓))
7		pm2.27 43	. . . . . . 7 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
8	7	anim2d 624	. . . . . 6 ⊢ (𝜑 → ((𝜃 ∧ (𝜑 → 𝜓)) → (𝜃 ∧ 𝜓)))
9	8	expdimp 458	. . . . 5 ⊢ ((𝜑 ∧ 𝜃) → ((𝜑 → 𝜓) → (𝜃 ∧ 𝜓)))
10	6, 9	syl5com 32	. . . 4 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓)))
11		ancr 556	. . . . 5 ⊢ ((𝜑 → 𝜒) → (𝜑 → (𝜒 ∧ 𝜑)))
12	11	anim1i 627	. . . 4 ⊢ (((𝜑 → 𝜒) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓))) → ((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓))))
13	4, 10, 12	syl2anc 596	. . 3 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓))))
14		con3 154	. . . . 5 ⊢ (((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓)) → (¬ (𝜃 ∧ 𝜓) → ¬ (𝜑 ∧ 𝜃)))
15		df-nan 1522	. . . . 5 ⊢ ((𝜃 ⊼ 𝜓) ↔ ¬ (𝜃 ∧ 𝜓))
16		df-nan 1522	. . . . 5 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
17	14, 15, 16	3imtr4g 299	. . . 4 ⊢ (((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓)) → ((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃)))
18	17	anim2i 629	. . 3 ⊢ (((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓))) → ((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃))))
19		nannan 1527	. . . . 5 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ↔ (𝜑 → (𝜒 ∧ 𝜑)))
20	19	biimpri 231	. . . 4 ⊢ ((𝜑 → (𝜒 ∧ 𝜑)) → (𝜑 ⊼ (𝜒 ⊼ 𝜑)))
21		nanim 1528	. . . . 5 ⊢ (((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃)) ↔ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
22	21	biimpi 219	. . . 4 ⊢ (((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃)) → ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
23	20, 22	anim12i 625	. . 3 ⊢ (((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃))) → ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
24	2, 13, 18, 23	4syl 20	. 2 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
25		nannan 1527	. 2 ⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))))
26	24, 25	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)