Theorem bilukdc 1391

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 139	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))
2	1	bibi1i 227	. . . . 5 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ ((𝜓 ↔ 𝜑) ↔ 𝜒))
3		biassdc 1390	. . . . . 6 ⊢ (DECID 𝜓 → (DECID 𝜑 → (DECID 𝜒 → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
4	3	imp31 254	. . . . 5 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
5	2, 4	syl5bb 191	. . . 4 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
6	5	ancom1s 564	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
7		dcbi 931	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ↔ 𝜓)))
8	7	imp 123	. . . . 5 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ↔ 𝜓))
9	8	adantr 274	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜓))
10		simpr 109	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜒)
11		dcbi 931	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜒 → DECID (𝜑 ↔ 𝜒)))
12		dcbi 931	. . . . . 6 ⊢ (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒))))
13	11, 12	syl9 72	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))))
14	13	imp31 254	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))
15		biassdc 1390	. . . 4 ⊢ (DECID (𝜑 ↔ 𝜓) → (DECID 𝜒 → (DECID (𝜓 ↔ (𝜑 ↔ 𝜒)) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))))
16	9, 10, 14, 15	syl3c 63	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
17	6, 16	mpbid 146	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
18		simplr 525	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜓)
19	11	imp 123	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
20	19	adantlr 474	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
21		biassdc 1390	. . 3 ⊢ (DECID 𝜒 → (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))))
22	10, 18, 20, 21	syl3c 63	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
23	17, 22	bitr4d 190	1 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒))))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704

This theorem depends on definitions:  df-bi 116  df-stab 826  df-dc 830

This theorem is referenced by: (None)