Theorem arg-ax 34605

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.)

Assertion

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

Proof of Theorem arg-ax

Step	Hyp	Ref	Expression
1		df-nan 1487	. . . . 5 ⊢ ((𝜃 ⊼ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
2		pm4.57 988	. . . . . . . 8 ⊢ (¬ (¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃)) ↔ ((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)))
3		orel2 888	. . . . . . . . . . . . 13 ⊢ (¬ 𝜑 → ((𝜒 ∨ 𝜑) → 𝜒))
4	3	com12 32	. . . . . . . . . . . 12 ⊢ ((𝜒 ∨ 𝜑) → (¬ 𝜑 → 𝜒))
5		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
6	5	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜒 ∨ 𝜑) → ((𝜓 ∧ 𝜒) → 𝜒))
7	4, 6	jad 187	. . . . . . . . . . 11 ⊢ ((𝜒 ∨ 𝜑) → ((𝜑 → (𝜓 ∧ 𝜒)) → 𝜒))
8	7	com12 32	. . . . . . . . . 10 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜒 ∨ 𝜑) → 𝜒))
9		pm3.45 622	. . . . . . . . . . . 12 ⊢ ((𝜒 → 𝜒) → ((𝜒 ∧ 𝜃) → (𝜒 ∧ 𝜃)))
10		pm3.45 622	. . . . . . . . . . . 12 ⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃)))
11	9, 10	anim12i 613	. . . . . . . . . . 11 ⊢ (((𝜒 → 𝜒) ∧ (𝜑 → 𝜒)) → (((𝜒 ∧ 𝜃) → (𝜒 ∧ 𝜃)) ∧ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃))))
12		jaob 959	. . . . . . . . . . 11 ⊢ (((𝜒 ∨ 𝜑) → 𝜒) ↔ ((𝜒 → 𝜒) ∧ (𝜑 → 𝜒)))
13		jaob 959	. . . . . . . . . . 11 ⊢ ((((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜒 ∧ 𝜃)) ↔ (((𝜒 ∧ 𝜃) → (𝜒 ∧ 𝜃)) ∧ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃))))
14	11, 12, 13	3imtr4i 292	. . . . . . . . . 10 ⊢ (((𝜒 ∨ 𝜑) → 𝜒) → (((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜒 ∧ 𝜃)))
15	8, 14	syl 17	. . . . . . . . 9 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜒 ∧ 𝜃)))
16		pm3.22 460	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝜃) → (𝜃 ∧ 𝜒))
17	15, 16	syl6 35	. . . . . . . 8 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜃 ∧ 𝜒)))
18	2, 17	syl5bi 241	. . . . . . 7 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (¬ (¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃)) → (𝜃 ∧ 𝜒)))
19	18	con1d 145	. . . . . 6 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (¬ (𝜃 ∧ 𝜒) → (¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃))))
20		df-nan 1487	. . . . . . . 8 ⊢ ((𝜒 ⊼ 𝜃) ↔ ¬ (𝜒 ∧ 𝜃))
21	20	biimpri 227	. . . . . . 7 ⊢ (¬ (𝜒 ∧ 𝜃) → (𝜒 ⊼ 𝜃))
22		df-nan 1487	. . . . . . . 8 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
23	22	biimpri 227	. . . . . . 7 ⊢ (¬ (𝜑 ∧ 𝜃) → (𝜑 ⊼ 𝜃))
24	21, 23	anim12i 613	. . . . . 6 ⊢ ((¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃)) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃)))
25	19, 24	syl6 35	. . . . 5 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (¬ (𝜃 ∧ 𝜒) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃))))
26	1, 25	syl5bi 241	. . . 4 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜃 ⊼ 𝜒) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃))))
27		nannan 1492	. . . 4 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
28		nannan 1492	. . . 4 ⊢ (((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ↔ ((𝜃 ⊼ 𝜒) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃))))
29	26, 27, 28	3imtr4i 292	. . 3 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
30	29	ancli 549	. 2 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
31		nannan 1492	. 2 ⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))))
32	30, 31	mpbir 230	1 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   ⊼ wnan 1486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-nan 1487

This theorem is referenced by: (None)