# Metamath Proof Explorer

## Theorem occon3

Description: Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014) (New usage is discouraged.)

Ref Expression
Assertion occon3
`|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) ) )`

### Proof

Step Hyp Ref Expression
1 ococss
` |-  ( B C_ ~H -> B C_ ( _|_ ` ( _|_ ` B ) ) )`
` |-  ( ( A C_ ~H /\ B C_ ~H ) -> B C_ ( _|_ ` ( _|_ ` B ) ) )`
3 ocss
` |-  ( B C_ ~H -> ( _|_ ` B ) C_ ~H )`
4 occon
` |-  ( ( A C_ ~H /\ ( _|_ ` B ) C_ ~H ) -> ( A C_ ( _|_ ` B ) -> ( _|_ ` ( _|_ ` B ) ) C_ ( _|_ ` A ) ) )`
5 3 4 sylan2
` |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) -> ( _|_ ` ( _|_ ` B ) ) C_ ( _|_ ` A ) ) )`
6 sstr2
` |-  ( B C_ ( _|_ ` ( _|_ ` B ) ) -> ( ( _|_ ` ( _|_ ` B ) ) C_ ( _|_ ` A ) -> B C_ ( _|_ ` A ) ) )`
7 2 5 6 sylsyld
` |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) -> B C_ ( _|_ ` A ) ) )`
8 ococss
` |-  ( A C_ ~H -> A C_ ( _|_ ` ( _|_ ` A ) ) )`
` |-  ( ( A C_ ~H /\ B C_ ~H ) -> A C_ ( _|_ ` ( _|_ ` A ) ) )`
10 id
` |-  ( B C_ ~H -> B C_ ~H )`
11 ocss
` |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )`
12 occon
` |-  ( ( B C_ ~H /\ ( _|_ ` A ) C_ ~H ) -> ( B C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` B ) ) )`
13 10 11 12 syl2anr
` |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( B C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` B ) ) )`
14 sstr2
` |-  ( A C_ ( _|_ ` ( _|_ ` A ) ) -> ( ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` B ) -> A C_ ( _|_ ` B ) ) )`
15 9 13 14 sylsyld
` |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( B C_ ( _|_ ` A ) -> A C_ ( _|_ ` B ) ) )`
16 7 15 impbid
` |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) ) )`