Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  atcvrj1 Structured version   Unicode version

Theorem atcvrj1 30155
 Description: Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.)
Hypotheses
Ref Expression
atcvrj1x.l
atcvrj1x.j
atcvrj1x.c
atcvrj1x.a
Assertion
Ref Expression
atcvrj1

Proof of Theorem atcvrj1
StepHypRef Expression
1 simp3l 985 . . . 4
2 hlatl 30085 . . . . . 6
323ad2ant1 978 . . . . 5
4 simp21 990 . . . . 5
5 simp23 992 . . . . 5
6 eqid 2435 . . . . . 6
7 eqid 2435 . . . . . 6
8 atcvrj1x.a . . . . . 6
96, 7, 8atnem0 30043 . . . . 5
103, 4, 5, 9syl3anc 1184 . . . 4
111, 10mpbid 202 . . 3
12 simp1 957 . . . 4
13 eqid 2435 . . . . . 6
1413, 8atbase 30014 . . . . 5
154, 14syl 16 . . . 4
16 atcvrj1x.j . . . . 5
17 atcvrj1x.c . . . . 5
1813, 16, 6, 7, 17, 8cvrp 30140 . . . 4
1912, 15, 5, 18syl3anc 1184 . . 3
2011, 19mpbid 202 . 2
21 simp3r 986 . . 3
22 atcvrj1x.l . . . . 5
2322, 16, 8hlatexchb2 30118 . . . 4