This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atabs2i

Description: Absorption of an incomparable atom. (Contributed by NM, 18-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses atabs.1 
|- A e. CH
atabs.2 
|- B e. CH
Assertion atabs2i 
|- ( C e. HAtoms -> ( -. C C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = A ) )

Proof

Step Hyp Ref Expression
1 atabs.1 
 |-  A e. CH
2 atabs.2 
 |-  B e. CH
3 1 2 chjcli 
 |-  ( A vH B ) e. CH
4 1 3 atabsi 
 |-  ( C e. HAtoms -> ( -. C C_ ( A vH ( A vH B ) ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A i^i ( A vH B ) ) ) )
5 1 1 2 chjassi 
 |-  ( ( A vH A ) vH B ) = ( A vH ( A vH B ) )
6 1 chjidmi 
 |-  ( A vH A ) = A
7 6 oveq1i 
 |-  ( ( A vH A ) vH B ) = ( A vH B )
8 5 7 eqtr3i 
 |-  ( A vH ( A vH B ) ) = ( A vH B )
9 8 sseq2i 
 |-  ( C C_ ( A vH ( A vH B ) ) <-> C C_ ( A vH B ) )
10 9 notbii 
 |-  ( -. C C_ ( A vH ( A vH B ) ) <-> -. C C_ ( A vH B ) )
11 1 2 chabs2i 
 |-  ( A i^i ( A vH B ) ) = A
12 11 eqeq2i 
 |-  ( ( ( A vH C ) i^i ( A vH B ) ) = ( A i^i ( A vH B ) ) <-> ( ( A vH C ) i^i ( A vH B ) ) = A )
13 4 10 12 3imtr3g 
 |-  ( C e. HAtoms -> ( -. C C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = A ) )