Theorem dn1dc 866

Description: DN₁ for decidable propositions. Without the decidability conditions, DN₁ can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)

Assertion

Ref	Expression
dn1dc	⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → (¬ (¬ (¬ (φ ∨ ψ) ∨ χ) ∨ ¬ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))) ↔ χ))

Proof of Theorem dn1dc

Step	Hyp	Ref	Expression
1		pm2.45 656	. . . . 5 ⊢ (¬ (φ ∨ ψ) → ¬ φ)
2		imnan 623	. . . . 5 ⊢ ((¬ (φ ∨ ψ) → ¬ φ) ↔ ¬ (¬ (φ ∨ ψ) ∧ φ))
3	1, 2	mpbi 133	. . . 4 ⊢ ¬ (¬ (φ ∨ ψ) ∧ φ)
4	3	biorfi 664	. . 3 ⊢ (χ ↔ (χ ∨ (¬ (φ ∨ ψ) ∧ φ)))
5		orcom 646	. . 3 ⊢ ((χ ∨ (¬ (φ ∨ ψ) ∧ φ)) ↔ ((¬ (φ ∨ ψ) ∧ φ) ∨ χ))
6		ordir 729	. . 3 ⊢ (((¬ (φ ∨ ψ) ∧ φ) ∨ χ) ↔ ((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ χ)))
7	4, 5, 6	3bitri 195	. 2 ⊢ (χ ↔ ((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ χ)))
8		pm4.45 697	. . . . . 6 ⊢ (χ ↔ (χ ∧ (χ ∨ θ)))
9		simprrl 491	. . . . . . 7 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID χ)
10		dcor 842	. . . . . . . . 9 ⊢ (DECID χ → (DECID θ → DECID (χ ∨ θ)))
11	10	imp 115	. . . . . . . 8 ⊢ ((DECID χ ∧ DECID θ) → DECID (χ ∨ θ))
12	11	ad2antll 460	. . . . . . 7 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID (χ ∨ θ))
13		anordc 862	. . . . . . 7 ⊢ (DECID χ → (DECID (χ ∨ θ) → ((χ ∧ (χ ∨ θ)) ↔ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))))
14	9, 12, 13	sylc 56	. . . . . 6 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → ((χ ∧ (χ ∨ θ)) ↔ ¬ (¬ χ ∨ ¬ (χ ∨ θ))))
15	8, 14	syl5bb 181	. . . . 5 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → (χ ↔ ¬ (¬ χ ∨ ¬ (χ ∨ θ))))
16	15	orbi2d 703	. . . 4 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → ((φ ∨ χ) ↔ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))))
17	16	anbi2d 437	. . 3 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → (((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ χ)) ↔ ((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ))))))
18		dcor 842	. . . . . . . 8 ⊢ (DECID φ → (DECID ψ → DECID (φ ∨ ψ)))
19		dcn 745	. . . . . . . 8 ⊢ (DECID (φ ∨ ψ) → DECID ¬ (φ ∨ ψ))
20	18, 19	syl6 29	. . . . . . 7 ⊢ (DECID φ → (DECID ψ → DECID ¬ (φ ∨ ψ)))
21	20	imp 115	. . . . . 6 ⊢ ((DECID φ ∧ DECID ψ) → DECID ¬ (φ ∨ ψ))
22	21	adantrr 448	. . . . 5 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID ¬ (φ ∨ ψ))
23		dcor 842	. . . . 5 ⊢ (DECID ¬ (φ ∨ ψ) → (DECID χ → DECID (¬ (φ ∨ ψ) ∨ χ)))
24	22, 9, 23	sylc 56	. . . 4 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID (¬ (φ ∨ ψ) ∨ χ))
25		dcn 745	. . . . . . . 8 ⊢ (DECID χ → DECID ¬ χ)
26	9, 25	syl 14	. . . . . . 7 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID ¬ χ)
27		dcn 745	. . . . . . . 8 ⊢ (DECID (χ ∨ θ) → DECID ¬ (χ ∨ θ))
28	12, 27	syl 14	. . . . . . 7 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID ¬ (χ ∨ θ))
29		dcor 842	. . . . . . 7 ⊢ (DECID ¬ χ → (DECID ¬ (χ ∨ θ) → DECID (¬ χ ∨ ¬ (χ ∨ θ))))
30	26, 28, 29	sylc 56	. . . . . 6 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID (¬ χ ∨ ¬ (χ ∨ θ)))
31		dcn 745	. . . . . 6 ⊢ (DECID (¬ χ ∨ ¬ (χ ∨ θ)) → DECID ¬ (¬ χ ∨ ¬ (χ ∨ θ)))
32	30, 31	syl 14	. . . . 5 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID ¬ (¬ χ ∨ ¬ (χ ∨ θ)))
33		dcor 842	. . . . . 6 ⊢ (DECID φ → (DECID ¬ (¬ χ ∨ ¬ (χ ∨ θ)) → DECID (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))))
34	33	imp 115	. . . . 5 ⊢ ((DECID φ ∧ DECID ¬ (¬ χ ∨ ¬ (χ ∨ θ))) → DECID (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ))))
35	32, 34	syldan 266	. . . 4 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → DECID (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ))))
36		anordc 862	. . . 4 ⊢ (DECID (¬ (φ ∨ ψ) ∨ χ) → (DECID (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ))) → (((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))) ↔ ¬ (¬ (¬ (φ ∨ ψ) ∨ χ) ∨ ¬ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))))))
37	24, 35, 36	sylc 56	. . 3 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → (((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))) ↔ ¬ (¬ (¬ (φ ∨ ψ) ∨ χ) ∨ ¬ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ))))))
38	17, 37	bitrd 177	. 2 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → (((¬ (φ ∨ ψ) ∨ χ) ∧ (φ ∨ χ)) ↔ ¬ (¬ (¬ (φ ∨ ψ) ∨ χ) ∨ ¬ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ))))))
39	7, 38	syl5rbb 182	1 ⊢ ((DECID φ ∧ (DECID ψ ∧ (DECID χ ∧ DECID θ))) → (¬ (¬ (¬ (φ ∨ ψ) ∨ χ) ∨ ¬ (φ ∨ ¬ (¬ χ ∨ ¬ (χ ∨ θ)))) ↔ χ))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628  DECID wdc 741

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 629

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

This theorem is referenced by: (None)