Metamath Proof Explorer


Theorem 4atexlemu

Description: Lemma for 4atexlem7 . (Contributed by NM, 23-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
4thatlem0.l ˙ = K
4thatlem0.j ˙ = join K
4thatlem0.m ˙ = meet K
4thatlem0.a A = Atoms K
4thatlem0.h H = LHyp K
4thatlem0.u U = P ˙ Q ˙ W
Assertion 4atexlemu φ U A

Proof

Step Hyp Ref Expression
1 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
2 4thatlem0.l ˙ = K
3 4thatlem0.j ˙ = join K
4 4thatlem0.m ˙ = meet K
5 4thatlem0.a A = Atoms K
6 4thatlem0.h H = LHyp K
7 4thatlem0.u U = P ˙ Q ˙ W
8 1 4atexlemk φ K HL
9 1 4atexlemw φ W H
10 1 4atexlempw φ P A ¬ P ˙ W
11 1 4atexlemq φ Q A
12 1 4atexlempnq φ P Q
13 2 3 4 5 6 7 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
14 8 9 10 11 12 13 syl212anc φ U A