![]() |
Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > QLE Home > Th. List > an1r | GIF version |
Description: Conjunction with 1. |
Ref | Expression |
---|---|
an1r | (1 ∩ a) = a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 74 | . 2 (1 ∩ a) = (a ∩ 1) | |
2 | an1 106 | . 2 (a ∩ 1) = a | |
3 | 1, 2 | ax-r2 36 | 1 (1 ∩ a) = a |
Colors of variables: term |
Syntax hints: = wb 1 ∩ wa 7 1wt 8 |
This theorem was proved from axioms: ax-a1 30 ax-a2 31 ax-a5 34 ax-r1 35 ax-r2 36 ax-r4 37 ax-r5 38 |
This theorem depends on definitions: df-a 40 df-t 41 df-f 42 |
This theorem is referenced by: ud3lem1c 568 ud3lem3 576 ud5lem1 589 i2i1i1 800 lem3.3.7i1e1 1060 lem3.3.7i1e2 1061 lem3.3.7i2e1 1063 lem3.3.7i2e2 1064 lem3.3.7i3e2 1067 lem3.3.7i4e2 1070 lem4.6.6i1j3 1092 dp15lema 1152 xdp15 1197 xxdp15 1200 xdp45lem 1202 xdp43lem 1203 xdp45 1204 xdp43 1205 3dp43 1206 |
Copyright terms: Public domain | W3C validator |