Theorem bilukdc 1407

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 140	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))
2	1	bibi1i 228	. . . . 5 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ ((𝜓 ↔ 𝜑) ↔ 𝜒))
3		biassdc 1406	. . . . . 6 ⊢ (DECID 𝜓 → (DECID 𝜑 → (DECID 𝜒 → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
4	3	imp31 256	. . . . 5 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜓 ↔ 𝜑) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
5	2, 4	bitrid 192	. . . 4 ⊢ (((DECID 𝜓 ∧ DECID 𝜑) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
6	5	ancom1s 569	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))
7		dcbi 938	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ↔ 𝜓)))
8	7	imp 124	. . . . 5 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ↔ 𝜓))
9	8	adantr 276	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜓))
10		simpr 110	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜒)
11		dcbi 938	. . . . . 6 ⊢ (DECID 𝜑 → (DECID 𝜒 → DECID (𝜑 ↔ 𝜒)))
12		dcbi 938	. . . . . 6 ⊢ (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒))))
13	11, 12	syl9 72	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → (DECID 𝜒 → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))))
14	13	imp31 256	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜓 ↔ (𝜑 ↔ 𝜒)))
15		biassdc 1406	. . . 4 ⊢ (DECID (𝜑 ↔ 𝜓) → (DECID 𝜒 → (DECID (𝜓 ↔ (𝜑 ↔ 𝜒)) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))))
16	9, 10, 14, 15	syl3c 63	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))) ↔ ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒))))))
17	6, 16	mpbid 147	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
18		simplr 528	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID 𝜓)
19	11	imp 124	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
20	19	adantlr 477	. . 3 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → DECID (𝜑 ↔ 𝜒))
21		biassdc 1406	. . 3 ⊢ (DECID 𝜒 → (DECID 𝜓 → (DECID (𝜑 ↔ 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))))
22	10, 18, 20, 21	syl3c 63	. 2 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒)) ↔ (𝜒 ↔ (𝜓 ↔ (𝜑 ↔ 𝜒)))))
23	17, 22	bitr4d 191	1 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒))))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  DECID wdc 835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836

This theorem is referenced by: (None)