Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biassdc | Unicode version |
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.) |
Ref | Expression |
---|---|
biassdc | DECID DECID DECID |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dc 743 | . . 3 DECID | |
2 | pm5.501 233 | . . . . . . 7 | |
3 | 2 | bibi1d 222 | . . . . . 6 |
4 | pm5.501 233 | . . . . . 6 | |
5 | 3, 4 | bitr3d 179 | . . . . 5 |
6 | 5 | a1d 22 | . . . 4 DECID DECID |
7 | nbbndc 1285 | . . . . . . . . 9 DECID DECID | |
8 | 7 | imp 115 | . . . . . . . 8 DECID DECID |
9 | 8 | adantl 262 | . . . . . . 7 DECID DECID |
10 | nbn2 613 | . . . . . . . . 9 | |
11 | 10 | bibi1d 222 | . . . . . . . 8 |
12 | 11 | adantr 261 | . . . . . . 7 DECID DECID |
13 | 9, 12 | bitr3d 179 | . . . . . 6 DECID DECID |
14 | nbn2 613 | . . . . . . 7 | |
15 | 14 | adantr 261 | . . . . . 6 DECID DECID |
16 | 13, 15 | bitr3d 179 | . . . . 5 DECID DECID |
17 | 16 | ex 108 | . . . 4 DECID DECID |
18 | 6, 17 | jaoi 636 | . . 3 DECID DECID |
19 | 1, 18 | sylbi 114 | . 2 DECID DECID DECID |
20 | 19 | expd 245 | 1 DECID DECID DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 97 wb 98 wo 629 DECID wdc 742 |
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 630 |
This theorem depends on definitions: df-bi 110 df-dc 743 |
This theorem is referenced by: bilukdc 1287 |
Copyright terms: Public domain | W3C validator |