Theorem biassdc 1395

Description: Associative law for the biconditional, for decidable propositions.

The classical version (without the decidability conditions) is an axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207-224, 2002, http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805, and, interestingly, was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (Contributed by Jim Kingdon, 4-May-2018.)

Assertion

Ref	Expression
biassdc	|- (DECID ph -> (DECID ps -> (DECID ch -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) ) )

Proof of Theorem biassdc

Step	Hyp	Ref	Expression
1		df-dc 835	. . 3 |- (DECID ph <-> ( ph \/ -. ph ) )
2		pm5.501 244	. . . . . . 7 |- ( ph -> ( ps <-> ( ph <-> ps ) ) )
3	2	bibi1d 233	. . . . . 6 |- ( ph -> ( ( ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
4		pm5.501 244	. . . . . 6 |- ( ph -> ( ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
5	3, 4	bitr3d 190	. . . . 5 |- ( ph -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
6	5	a1d 22	. . . 4 |- ( ph -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
7		nbbndc 1394	. . . . . . . . 9 |- (DECID ps -> (DECID ch -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) ) )
8	7	imp 124	. . . . . . . 8 |- ( (DECID ps /\ DECID ch ) -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) )
9	8	adantl 277	. . . . . . 7 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) )
10		nbn2 697	. . . . . . . . 9 |- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )
11	10	bibi1d 233	. . . . . . . 8 |- ( -. ph -> ( ( -. ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
12	11	adantr 276	. . . . . . 7 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( -. ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
13	9, 12	bitr3d 190	. . . . . 6 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( -. ( ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
14		nbn2 697	. . . . . . 7 |- ( -. ph -> ( -. ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
15	14	adantr 276	. . . . . 6 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( -. ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
16	13, 15	bitr3d 190	. . . . 5 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
17	16	ex 115	. . . 4 |- ( -. ph -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
18	6, 17	jaoi 716	. . 3 |- ( ( ph \/ -. ph ) -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
19	1, 18	sylbi 121	. 2 |- (DECID ph -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
20	19	expd 258	1 |- (DECID ph -> (DECID ps -> (DECID ch -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 708  DECID wdc 834

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 614  ax-in2 615  ax-io 709

This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835

This theorem is referenced by:  bilukdc  1396