Description: One of the conditions showing CH is an ortholattice. (This corresponds to axiom "ax-r5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | qlaxr5.1 | |- A e. CH |
|
| qlaxr5.2 | |- B e. CH |
||
| qlaxr5.3 | |- C e. CH |
||
| qlaxr5.4 | |- A = B |
||
| Assertion | qlaxr5i | |- ( A vH C ) = ( B vH C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qlaxr5.1 | |- A e. CH |
|
| 2 | qlaxr5.2 | |- B e. CH |
|
| 3 | qlaxr5.3 | |- C e. CH |
|
| 4 | qlaxr5.4 | |- A = B |
|
| 5 | 4 | oveq1i | |- ( A vH C ) = ( B vH C ) |