Theorem bilukdc 1327

Description: Lukasiewicz's shortest axiom for equivalential calculus (but modified to require decidable propositions). Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by Jim Kingdon, 5-May-2018.)

Assertion

Ref	Expression
bilukdc	⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒))))

Proof of Theorem bilukdc

Step	Hyp	Ref	Expression
1		bicom 138	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))
2	1	bibi1i 226	. . . . 5 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ ((𝜓 ↔ 𝜑) ↔ 𝜒))
3		biassdc 1326	. . . . . 6 ⊢ (DECID 𝜓 → (DECID 𝜑 → (DECID 𝜒 → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
4	3	imp31 252	. . . . 5 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
5	2, 4	syl5bb 190	. . . 4 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
6	5	ancom1s 533	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
7		dcbi 877	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ↔ 𝜓)))
8	7	imp 122	. . . . 5 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ↔ 𝜓))
9	8	adantr 270	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜓))
10		simpr 108	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜒)
11		dcbi 877	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜒 → DECID (𝜑 ↔ 𝜒)))
12		dcbi 877	. . . . . 6 ⊢ (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒))))
13	11, 12	syl9 71	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))))
14	13	imp31 252	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))
15		biassdc 1326	. . . 4 ⊢ (DECID (𝜑 ↔ 𝜓) → (DECID 𝜒 → (DECID (𝜓 ↔ (𝜑 ↔ 𝜒)) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))))
16	9, 10, 14, 15	syl3c 62	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
17	6, 16	mpbid 145	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
18		simplr 496	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜓)
19	11	imp 122	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
20	19	adantlr 460	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
21		biassdc 1326	. . 3 ⊢ (DECID 𝜒 → (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))))
22	10, 18, 20, 21	syl3c 62	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
23	17, 22	bitr4d 189	1 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒))))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103  DECID wdc 775

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662

This theorem depends on definitions:  df-bi 115  df-dc 776

This theorem is referenced by: (None)