Theorem biassdc 1341

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 787	. . 3 |- (DECID ph <-> ( ph \/ -. ph ) )
2		pm5.501 243	. . . . . . 7 |- ( ph -> ( ps <-> ( ph <-> ps ) ) )
3	2	bibi1d 232	. . . . . 6 |- ( ph -> ( ( ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
4		pm5.501 243	. . . . . 6 |- ( ph -> ( ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
5	3, 4	bitr3d 189	. . . . 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 1340	. . . . . . . . 9 |- (DECID ps -> (DECID ch -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) ) )
8	7	imp 123	. . . . . . . 8 |- ( (DECID ps /\ DECID ch ) -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) )
9	8	adantl 273	. . . . . . 7 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) )
10		nbn2 654	. . . . . . . . 9 |- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )
11	10	bibi1d 232	. . . . . . . 8 |- ( -. ph -> ( ( -. ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
12	11	adantr 272	. . . . . . 7 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( -. ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
13	9, 12	bitr3d 189	. . . . . 6 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( -. ( ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
14		nbn2 654	. . . . . . 7 |- ( -. ph -> ( -. ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
15	14	adantr 272	. . . . . 6 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( -. ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
16	13, 15	bitr3d 189	. . . . 5 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
17	16	ex 114	. . . 4 |- ( -. ph -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
18	6, 17	jaoi 677	. . 3 |- ( ( ph \/ -. ph ) -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
19	1, 18	sylbi 120	. 2 |- (DECID ph -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
20	19	expd 256	1 |- (DECID ph -> (DECID ps -> (DECID ch -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 670  DECID wdc 786

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

This theorem depends on definitions:  df-bi 116  df-dc 787

This theorem is referenced by:  bilukdc  1342