Metamath Proof Explorer


Theorem lhpex2leN

Description: There exist at least two different atoms under a co-atom. This allows us to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lhp2at.l ˙ = K
lhp2at.a A = Atoms K
lhp2at.h H = LHyp K
Assertion lhpex2leN K HL W H p A q A p ˙ W q ˙ W p q

Proof

Step Hyp Ref Expression
1 lhp2at.l ˙ = K
2 lhp2at.a A = Atoms K
3 lhp2at.h H = LHyp K
4 simprr K HL W H p A p ˙ W p ˙ W
5 1 2 3 lhpexle1 K HL W H q A q ˙ W q p
6 5 adantr K HL W H p A p ˙ W q A q ˙ W q p
7 4 6 jca K HL W H p A p ˙ W p ˙ W q A q ˙ W q p
8 necom p q q p
9 8 3anbi3i p ˙ W q ˙ W p q p ˙ W q ˙ W q p
10 3anass p ˙ W q ˙ W q p p ˙ W q ˙ W q p
11 9 10 bitri p ˙ W q ˙ W p q p ˙ W q ˙ W q p
12 11 rexbii q A p ˙ W q ˙ W p q q A p ˙ W q ˙ W q p
13 r19.42v q A p ˙ W q ˙ W q p p ˙ W q A q ˙ W q p
14 12 13 bitr2i p ˙ W q A q ˙ W q p q A p ˙ W q ˙ W p q
15 7 14 sylib K HL W H p A p ˙ W q A p ˙ W q ˙ W p q
16 1 2 3 lhpexle K HL W H p A p ˙ W
17 15 16 reximddv K HL W H p A q A p ˙ W q ˙ W p q