Theorem biassdc 1327

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 777	. . 3 |- (DECID ph <-> ( ph \/ -. ph ) )
2		pm5.501 242	. . . . . . 7 |- ( ph -> ( ps <-> ( ph <-> ps ) ) )
3	2	bibi1d 231	. . . . . 6 |- ( ph -> ( ( ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
4		pm5.501 242	. . . . . 6 |- ( ph -> ( ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
5	3, 4	bitr3d 188	. . . . 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 1326	. . . . . . . . 9 |- (DECID ps -> (DECID ch -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) ) )
8	7	imp 122	. . . . . . . 8 |- ( (DECID ps /\ DECID ch ) -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) )
9	8	adantl 271	. . . . . . 7 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( -. ps <-> ch ) <-> -. ( ps <-> ch ) ) )
10		nbn2 646	. . . . . . . . 9 |- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )
11	10	bibi1d 231	. . . . . . . 8 |- ( -. ph -> ( ( -. ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
12	11	adantr 270	. . . . . . 7 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( -. ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
13	9, 12	bitr3d 188	. . . . . 6 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( -. ( ps <-> ch ) <-> ( ( ph <-> ps ) <-> ch ) ) )
14		nbn2 646	. . . . . . 7 |- ( -. ph -> ( -. ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
15	14	adantr 270	. . . . . 6 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( -. ( ps <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
16	13, 15	bitr3d 188	. . . . 5 |- ( ( -. ph /\ (DECID ps /\ DECID ch ) ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) )
17	16	ex 113	. . . 4 |- ( -. ph -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
18	6, 17	jaoi 669	. . 3 |- ( ( ph \/ -. ph ) -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
19	1, 18	sylbi 119	. 2 |- (DECID ph -> ( (DECID ps /\ DECID ch ) -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) )
20	19	expd 254	1 |- (DECID ph -> (DECID ps -> (DECID ch -> ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 102   <-> wb 103   \/ wo 662  DECID wdc 776

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663

This theorem depends on definitions:  df-bi 115  df-dc 777

This theorem is referenced by:  bilukdc  1328