Theorem atcvat2i

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	atoml.1	|- A e. CH
Assertion	atcvat2i	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A A e. HAtoms ) )

Proof

Step	Hyp	Ref	Expression
1		atoml.1	|- A e. CH
2		atcv1	|- ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ A ( A = 0H <-> B = C ) )
3	1 2	mp3anl1	|- ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A ( A = 0H <-> B = C ) )
4	3	necon3abid	|- ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A ( A =/= 0H <-> -. B = C ) )
5		atelch	|- ( B e. HAtoms -> B e. CH )
6		atelch	|- ( C e. HAtoms -> C e. CH )
7		chjcl	|- ( ( B e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
8	5 6 7	syl2an	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( B vH C ) e. CH )
9		cvpss	|- ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( A A C. ( B vH C ) ) )
10	1 8 9	sylancr	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A A C. ( B vH C ) ) )
11	1	atcvati	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( B vH C ) ) -> A e. HAtoms ) )
12	11	expcomd	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A C. ( B vH C ) -> ( A =/= 0H -> A e. HAtoms ) ) )
13	10 12	syld	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A ( A =/= 0H -> A e. HAtoms ) ) )
14	13	imp	|- ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A ( A =/= 0H -> A e. HAtoms ) )
15	4 14	sylbird	|- ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A ( -. B = C -> A e. HAtoms ) )
16	15	ex	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A ( -. B = C -> A e. HAtoms ) ) )
17	16	com23	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( -. B = C -> ( A A e. HAtoms ) ) )
18	17	impd	|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A A e. HAtoms ) )