Theorem arg-ax

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

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

Proof

Step	Hyp	Ref	Expression
1		df-nan	⊢ ( ( 𝜃 ⊼ 𝜒 ) ↔ ¬ ( 𝜃 ∧ 𝜒 ) )
2		pm4.57	⊢ ( ¬ ( ¬ ( 𝜒 ∧ 𝜃 ) ∧ ¬ ( 𝜑 ∧ 𝜃 ) ) ↔ ( ( 𝜒 ∧ 𝜃 ) ∨ ( 𝜑 ∧ 𝜃 ) ) )
3		orel2	⊢ ( ¬ 𝜑 → ( ( 𝜒 ∨ 𝜑 ) → 𝜒 ) )
4	3	com12	⊢ ( ( 𝜒 ∨ 𝜑 ) → ( ¬ 𝜑 → 𝜒 ) )
5		simpr	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜒 )
6	5	a1i	⊢ ( ( 𝜒 ∨ 𝜑 ) → ( ( 𝜓 ∧ 𝜒 ) → 𝜒 ) )
7	4 6	jad	⊢ ( ( 𝜒 ∨ 𝜑 ) → ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → 𝜒 ) )
8	7	com12	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜒 ∨ 𝜑 ) → 𝜒 ) )
9		pm3.45	⊢ ( ( 𝜒 → 𝜒 ) → ( ( 𝜒 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜃 ) ) )
10		pm3.45	⊢ ( ( 𝜑 → 𝜒 ) → ( ( 𝜑 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜃 ) ) )
11	9 10	anim12i	⊢ ( ( ( 𝜒 → 𝜒 ) ∧ ( 𝜑 → 𝜒 ) ) → ( ( ( 𝜒 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜃 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜃 ) ) ) )
12		jaob	⊢ ( ( ( 𝜒 ∨ 𝜑 ) → 𝜒 ) ↔ ( ( 𝜒 → 𝜒 ) ∧ ( 𝜑 → 𝜒 ) ) )
13		jaob	⊢ ( ( ( ( 𝜒 ∧ 𝜃 ) ∨ ( 𝜑 ∧ 𝜃 ) ) → ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( ( 𝜒 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜃 ) ) ∧ ( ( 𝜑 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜃 ) ) ) )
14	11 12 13	3imtr4i	⊢ ( ( ( 𝜒 ∨ 𝜑 ) → 𝜒 ) → ( ( ( 𝜒 ∧ 𝜃 ) ∨ ( 𝜑 ∧ 𝜃 ) ) → ( 𝜒 ∧ 𝜃 ) ) )
15	8 14	syl	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( ( 𝜒 ∧ 𝜃 ) ∨ ( 𝜑 ∧ 𝜃 ) ) → ( 𝜒 ∧ 𝜃 ) ) )
16		pm3.22	⊢ ( ( 𝜒 ∧ 𝜃 ) → ( 𝜃 ∧ 𝜒 ) )
17	15 16	syl6	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( ( 𝜒 ∧ 𝜃 ) ∨ ( 𝜑 ∧ 𝜃 ) ) → ( 𝜃 ∧ 𝜒 ) ) )
18	2 17	biimtrid	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ¬ ( ¬ ( 𝜒 ∧ 𝜃 ) ∧ ¬ ( 𝜑 ∧ 𝜃 ) ) → ( 𝜃 ∧ 𝜒 ) ) )
19	18	con1d	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ¬ ( 𝜃 ∧ 𝜒 ) → ( ¬ ( 𝜒 ∧ 𝜃 ) ∧ ¬ ( 𝜑 ∧ 𝜃 ) ) ) )
20		df-nan	⊢ ( ( 𝜒 ⊼ 𝜃 ) ↔ ¬ ( 𝜒 ∧ 𝜃 ) )
21	20	biimpri	⊢ ( ¬ ( 𝜒 ∧ 𝜃 ) → ( 𝜒 ⊼ 𝜃 ) )
22		df-nan	⊢ ( ( 𝜑 ⊼ 𝜃 ) ↔ ¬ ( 𝜑 ∧ 𝜃 ) )
23	22	biimpri	⊢ ( ¬ ( 𝜑 ∧ 𝜃 ) → ( 𝜑 ⊼ 𝜃 ) )
24	21 23	anim12i	⊢ ( ( ¬ ( 𝜒 ∧ 𝜃 ) ∧ ¬ ( 𝜑 ∧ 𝜃 ) ) → ( ( 𝜒 ⊼ 𝜃 ) ∧ ( 𝜑 ⊼ 𝜃 ) ) )
25	19 24	syl6	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ¬ ( 𝜃 ∧ 𝜒 ) → ( ( 𝜒 ⊼ 𝜃 ) ∧ ( 𝜑 ⊼ 𝜃 ) ) ) )
26	1 25	biimtrid	⊢ ( ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜃 ⊼ 𝜒 ) → ( ( 𝜒 ⊼ 𝜃 ) ∧ ( 𝜑 ⊼ 𝜃 ) ) ) )
27		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ↔ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) )
28		nannan	⊢ ( ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜒 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ↔ ( ( 𝜃 ⊼ 𝜒 ) → ( ( 𝜒 ⊼ 𝜃 ) ∧ ( 𝜑 ⊼ 𝜃 ) ) ) )
29	26 27 28	3imtr4i	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜒 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
30	29	ancli	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ∧ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜒 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )
31		nannan	⊢ ( ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜒 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) ↔ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) → ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ∧ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜒 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) )
32	30 31	mpbir	⊢ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜒 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜒 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )