Theorem arg-ax 37126

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 1522	. . . . 5 ⊢ ((𝜃 ⊼ 𝜒) ↔ ¬ (𝜃 ∧ 𝜒))
2		pm4.57 1006	. . . . . . . 8 ⊢ (¬ (¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃)) ↔ ((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)))
3		orel2 904	. . . . . . . . . . . . 13 ⊢ (¬ 𝜑 → ((𝜒 ∨ 𝜑) → 𝜒))
4	3	com12 33	. . . . . . . . . . . 12 ⊢ ((𝜒 ∨ 𝜑) → (¬ 𝜑 → 𝜒))
5		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
6	5	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜒 ∨ 𝜑) → ((𝜓 ∧ 𝜒) → 𝜒))
7	4, 6	jad 189	. . . . . . . . . . 11 ⊢ ((𝜒 ∨ 𝜑) → ((𝜑 → (𝜓 ∧ 𝜒)) → 𝜒))
8	7	com12 33	. . . . . . . . . 10 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜒 ∨ 𝜑) → 𝜒))
9		pm3.45 634	. . . . . . . . . . . 12 ⊢ ((𝜒 → 𝜒) → ((𝜒 ∧ 𝜃) → (𝜒 ∧ 𝜃)))
10		pm3.45 634	. . . . . . . . . . . 12 ⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃)))
11	9, 10	anim12i 625	. . . . . . . . . . 11 ⊢ (((𝜒 → 𝜒) ∧ (𝜑 → 𝜒)) → (((𝜒 ∧ 𝜃) → (𝜒 ∧ 𝜃)) ∧ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃))))
12		jaob 976	. . . . . . . . . . 11 ⊢ (((𝜒 ∨ 𝜑) → 𝜒) ↔ ((𝜒 → 𝜒) ∧ (𝜑 → 𝜒)))
13		jaob 976	. . . . . . . . . . 11 ⊢ ((((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜒 ∧ 𝜃)) ↔ (((𝜒 ∧ 𝜃) → (𝜒 ∧ 𝜃)) ∧ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃))))
14	11, 12, 13	3imtr4i 295	. . . . . . . . . 10 ⊢ (((𝜒 ∨ 𝜑) → 𝜒) → (((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜒 ∧ 𝜃)))
15	8, 14	syl 18	. . . . . . . . 9 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜒 ∧ 𝜃)))
16		pm3.22 465	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝜃) → (𝜃 ∧ 𝜒))
17	15, 16	syl6 36	. . . . . . . 8 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (((𝜒 ∧ 𝜃) ∨ (𝜑 ∧ 𝜃)) → (𝜃 ∧ 𝜒)))
18	2, 17	biimtrid 245	. . . . . . 7 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (¬ (¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃)) → (𝜃 ∧ 𝜒)))
19	18	con1d 146	. . . . . 6 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (¬ (𝜃 ∧ 𝜒) → (¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃))))
20		df-nan 1522	. . . . . . . 8 ⊢ ((𝜒 ⊼ 𝜃) ↔ ¬ (𝜒 ∧ 𝜃))
21	20	biimpri 231	. . . . . . 7 ⊢ (¬ (𝜒 ∧ 𝜃) → (𝜒 ⊼ 𝜃))
22		df-nan 1522	. . . . . . . 8 ⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃))
23	22	biimpri 231	. . . . . . 7 ⊢ (¬ (𝜑 ∧ 𝜃) → (𝜑 ⊼ 𝜃))
24	21, 23	anim12i 625	. . . . . 6 ⊢ ((¬ (𝜒 ∧ 𝜃) ∧ ¬ (𝜑 ∧ 𝜃)) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃)))
25	19, 24	syl6 36	. . . . 5 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (¬ (𝜃 ∧ 𝜒) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃))))
26	1, 25	biimtrid 245	. . . 4 ⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜃 ⊼ 𝜒) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃))))
27		nannan 1527	. . . 4 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
28		nannan 1527	. . . 4 ⊢ (((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ↔ ((𝜃 ⊼ 𝜒) → ((𝜒 ⊼ 𝜃) ∧ (𝜑 ⊼ 𝜃))))
29	26, 27, 28	3imtr4i 295	. . 3 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))
30	29	ancli 558	. 2 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
31		nannan 1527	. 2 ⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ∧ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))))
32	30, 31	mpbir 234	1 ⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   ⊼ 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-or 862  df-nan 1522

This theorem is used by: (None)