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 ) )