Metamath Proof Explorer


Theorem 4atexlempns

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
4thatlemslps.l ˙ = K
4thatlemslps.j ˙ = join K
4thatlemslps.a A = Atoms K
Assertion 4atexlempns φ P S

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 4thatlemslps.l ˙ = K
3 4thatlemslps.j ˙ = join K
4 4thatlemslps.a A = Atoms K
5 1 4atexlemk φ K HL
6 1 4atexlemp φ P A
7 1 4atexlemq φ Q A
8 1 4atexlems φ S A
9 1 4atexlemnslpq φ ¬ S ˙ P ˙ Q
10 2 3 4 4atlem0be K HL P A Q A S A ¬ S ˙ P ˙ Q P S
11 5 6 7 8 9 10 syl131anc φ P S