Description: One of the conditions showing CH is an ortholattice. (This corresponds to axiom "ax-r4" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | qlaxr4.1 | |- A e. CH |
|
| qlaxr4.2 | |- B e. CH |
||
| qlaxr4.3 | |- A = B |
||
| Assertion | qlaxr4i | |- ( _|_ ` A ) = ( _|_ ` B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qlaxr4.1 | |- A e. CH |
|
| 2 | qlaxr4.2 | |- B e. CH |
|
| 3 | qlaxr4.3 | |- A = B |
|
| 4 | 3 | fveq2i | |- ( _|_ ` A ) = ( _|_ ` B ) |