Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > com2or | Unicode version |
Description: Th. 4.2 Beran p. 49. |
Ref | Expression |
---|---|
fh.1 | |
fh.2 |
Ref | Expression |
---|---|
com2or |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fh.1 | . . . . . . . . 9 | |
2 | 1 | comcom 453 | . . . . . . . 8 |
3 | 2 | df-c2 133 | . . . . . . 7 |
4 | ancom 74 | . . . . . . . 8 | |
5 | ancom 74 | . . . . . . . 8 | |
6 | 4, 5 | 2or 72 | . . . . . . 7 |
7 | 3, 6 | ax-r2 36 | . . . . . 6 |
8 | fh.2 | . . . . . . . . 9 | |
9 | 8 | comcom 453 | . . . . . . . 8 |
10 | 9 | df-c2 133 | . . . . . . 7 |
11 | ancom 74 | . . . . . . . 8 | |
12 | ancom 74 | . . . . . . . 8 | |
13 | 11, 12 | 2or 72 | . . . . . . 7 |
14 | 10, 13 | ax-r2 36 | . . . . . 6 |
15 | 7, 14 | 2or 72 | . . . . 5 |
16 | or4 84 | . . . . 5 | |
17 | 15, 16 | ax-r2 36 | . . . 4 |
18 | ancom 74 | . . . . . . 7 | |
19 | 1, 8 | fh1 469 | . . . . . . 7 |
20 | 18, 19 | ax-r2 36 | . . . . . 6 |
21 | ancom 74 | . . . . . . 7 | |
22 | 1 | comcom3 454 | . . . . . . . 8 |
23 | 8 | comcom3 454 | . . . . . . . 8 |
24 | 22, 23 | fh1 469 | . . . . . . 7 |
25 | 21, 24 | ax-r2 36 | . . . . . 6 |
26 | 20, 25 | 2or 72 | . . . . 5 |
27 | 26 | ax-r1 35 | . . . 4 |
28 | 17, 27 | ax-r2 36 | . . 3 |
29 | 28 | df-c1 132 | . 2 |
30 | 29 | comcom 453 | 1 |
Copyright terms: Public domain | W3C validator |