Theorem lukshef-ax2

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)

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

Proof

Step	Hyp	Ref	Expression
1		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) )
2	1	biimpi	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) )
3		simpr	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜒 )
4	3	imim2i	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( 𝜑 → 𝜒 ) )
5		simpl	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜓 )
6	5	imim2i	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( 𝜑 → 𝜓 ) )
7		pm2.27	⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
8	7	anim2d	⊢ ( 𝜑 → ( ( 𝜃 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜃 ∧ 𝜓 ) ) )
9	8	expdimp	⊢ ( ( 𝜑 ∧ 𝜃 ) → ( ( 𝜑 → 𝜓 ) → ( 𝜃 ∧ 𝜓 ) ) )
10	6 9	syl5com	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜓 ) ) )
11		ancr	⊢ ( ( 𝜑 → 𝜒 ) → ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) )
12	11	anim1i	⊢ ( ( ( 𝜑 → 𝜒 ) ∧ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜓 ) ) ) → ( ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜓 ) ) ) )
13	4 10 12	syl2anc	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜓 ) ) ) )
14		con3	⊢ ( ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜓 ) ) → ( ¬ ( 𝜃 ∧ 𝜓 ) → ¬ ( 𝜑 ∧ 𝜃 ) ) )
15		df-nan	⊢ ( ( 𝜃 ⊼ 𝜓 ) ↔ ¬ ( 𝜃 ∧ 𝜓 ) )
16		df-nan	⊢ ( ( 𝜑 ⊼ 𝜃 ) ↔ ¬ ( 𝜑 ∧ 𝜃 ) )
17	14 15 16	3imtr4g	⊢ ( ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜓 ) ) → ( ( 𝜃 ⊼ 𝜓 ) → ( 𝜑 ⊼ 𝜃 ) ) )
18	17	anim2i	⊢ ( ( ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜓 ) ) ) → ( ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) ∧ ( ( 𝜃 ⊼ 𝜓 ) → ( 𝜑 ⊼ 𝜃 ) ) ) )
19		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜑 ) ) ↔ ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) )
20	19	biimpri	⊢ ( ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) → ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜑 ) ) )
21		nanim	⊢ ( ( ( 𝜃 ⊼ 𝜓 ) → ( 𝜑 ⊼ 𝜃 ) ) ↔ ( ( 𝜃 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
22	21	biimpi	⊢ ( ( ( 𝜃 ⊼ 𝜓 ) → ( 𝜑 ⊼ 𝜃 ) ) → ( ( 𝜃 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
23	20 22	anim12i	⊢ ( ( ( 𝜑 → ( 𝜒 ∧ 𝜑 ) ) ∧ ( ( 𝜃 ⊼ 𝜓 ) → ( 𝜑 ⊼ 𝜃 ) ) ) → ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜑 ) ) ∧ ( ( 𝜃 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )
24	2 13 18 23	4syl	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜑 ) ) ∧ ( ( 𝜃 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )
25		nannan	⊢ ( ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜑 ) ) ⊼ ( ( 𝜃 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) ↔ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜑 ) ) ∧ ( ( 𝜃 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) )
26	24 25	mpbir	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜑 ) ) ⊼ ( ( 𝜃 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )