Theorem bilukdc 1287

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 128	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))
2	1	bibi1i 217	. . . . 5 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ ((𝜓 ↔ 𝜑) ↔ 𝜒))
3		biassdc 1286	. . . . . 6 ⊢ (DECID 𝜓 → (DECID 𝜑 → (DECID 𝜒 → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
4	3	imp31 243	. . . . 5 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
5	2, 4	syl5bb 181	. . . 4 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
6	5	ancom1s 503	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
7		dcbi 844	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ↔ 𝜓)))
8	7	imp 115	. . . . 5 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ↔ 𝜓))
9	8	adantr 261	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜓))
10		simpr 103	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜒)
11		dcbi 844	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜒 → DECID (𝜑 ↔ 𝜒)))
12		dcbi 844	. . . . . 6 ⊢ (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒))))
13	11, 12	syl9 66	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))))
14	13	imp31 243	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))
15		biassdc 1286	. . . 4 ⊢ (DECID (𝜑 ↔ 𝜓) → (DECID 𝜒 → (DECID (𝜓 ↔ (𝜑 ↔ 𝜒)) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))))
16	9, 10, 14, 15	syl3c 57	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
17	6, 16	mpbid 135	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
18		simplr 482	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜓)
19	11	imp 115	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
20	19	adantlr 446	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
21		biassdc 1286	. . 3 ⊢ (DECID 𝜒 → (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))))
22	10, 18, 20, 21	syl3c 57	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
23	17, 22	bitr4d 180	1 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒))))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  DECID wdc 742

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630

This theorem depends on definitions:  df-bi 110  df-dc 743

This theorem is referenced by: (None)