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 776 | . . 3 DECID | |
2 | pm5.501 242 | . . . . . . 7 | |
3 | 2 | bibi1d 231 | . . . . . 6 |
4 | pm5.501 242 | . . . . . 6 | |
5 | 3, 4 | bitr3d 188 | . . . . 5 |
6 | 5 | a1d 22 | . . . 4 DECID DECID |
7 | nbbndc 1325 | . . . . . . . . 9 DECID DECID | |
8 | 7 | imp 122 | . . . . . . . 8 DECID DECID |
9 | 8 | adantl 271 | . . . . . . 7 DECID DECID |
10 | nbn2 645 | . . . . . . . . 9 | |
11 | 10 | bibi1d 231 | . . . . . . . 8 |
12 | 11 | adantr 270 | . . . . . . 7 DECID DECID |
13 | 9, 12 | bitr3d 188 | . . . . . 6 DECID DECID |
14 | nbn2 645 | . . . . . . 7 | |
15 | 14 | adantr 270 | . . . . . 6 DECID DECID |
16 | 13, 15 | bitr3d 188 | . . . . 5 DECID DECID |
17 | 16 | ex 113 | . . . 4 DECID DECID |
18 | 6, 17 | jaoi 668 | . . 3 DECID DECID |
19 | 1, 18 | sylbi 119 | . 2 DECID DECID DECID |
20 | 19 | expd 254 | 1 DECID DECID DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 102 wb 103 wo 661 DECID wdc 775 |
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 576 ax-in2 577 ax-io 662 |
This theorem depends on definitions: df-bi 115 df-dc 776 |
This theorem is referenced by: bilukdc 1327 |
Copyright terms: Public domain | W3C validator |