Theorem waj-ax

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)

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

Proof

Step	Hyp	Ref	Expression
1		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) )
2		simpr	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜒 )
3	2	imim2i	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( 𝜑 → 𝜒 ) )
4		pm2.27	⊢ ( 𝜑 → ( ( 𝜑 → 𝜒 ) → 𝜒 ) )
5	4	anim2d	⊢ ( 𝜑 → ( ( 𝜃 ∧ ( 𝜑 → 𝜒 ) ) → ( 𝜃 ∧ 𝜒 ) ) )
6	5	expdimp	⊢ ( ( 𝜑 ∧ 𝜃 ) → ( ( 𝜑 → 𝜒 ) → ( 𝜃 ∧ 𝜒 ) ) )
7	3 6	syl5com	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜒 ) ) )
8	7	con3d	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ¬ ( 𝜃 ∧ 𝜒 ) → ¬ ( 𝜑 ∧ 𝜃 ) ) )
9		df-nan	⊢ ( ( 𝜃 ⊼ 𝜒 ) ↔ ¬ ( 𝜃 ∧ 𝜒 ) )
10		df-nan	⊢ ( ( 𝜑 ⊼ 𝜃 ) ↔ ¬ ( 𝜑 ∧ 𝜃 ) )
11	8 9 10	3imtr4g	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜃 ⊼ 𝜒 ) → ( 𝜑 ⊼ 𝜃 ) ) )
12		nanim	⊢ ( ( ( 𝜃 ⊼ 𝜒 ) → ( 𝜑 ⊼ 𝜃 ) ) ↔ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
13	11 12	sylib	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
14		pm3.21	⊢ ( 𝜓 → ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) )
15	14	adantr	⊢ ( ( 𝜓 ∧ 𝜒 ) → ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) )
16	15	com12	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → ( 𝜑 ∧ 𝜓 ) ) )
17	16	a2i	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) )
18		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜑 ⊼ 𝜓 ) ) ↔ ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) )
19	17 18	sylibr	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( 𝜑 ⊼ ( 𝜑 ⊼ 𝜓 ) ) )
20	13 19	jca	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ∧ ( 𝜑 ⊼ ( 𝜑 ⊼ 𝜓 ) ) ) )
21	1 20	sylbi	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ∧ ( 𝜑 ⊼ ( 𝜑 ⊼ 𝜓 ) ) ) )
22		nannan	⊢ ( ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ⊼ ( 𝜑 ⊼ ( 𝜑 ⊼ 𝜓 ) ) ) ) ↔ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ∧ ( 𝜑 ⊼ ( 𝜑 ⊼ 𝜓 ) ) ) ) )
23	21 22	mpbir	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ⊼ ( 𝜑 ⊼ ( 𝜑 ⊼ 𝜓 ) ) ) )