Metamath Proof Explorer


Theorem dalem41

Description: Lemma for dath . (Contributed by NM, 4-Aug-2012)

Ref Expression
Hypotheses dalem.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
dalem.l ˙ = K
dalem.j ˙ = join K
dalem.a A = Atoms K
dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
dalem38.m ˙ = meet K
dalem38.o O = LPlanes K
dalem38.y Y = P ˙ Q ˙ R
dalem38.z Z = S ˙ T ˙ U
dalem38.g G = c ˙ P ˙ d ˙ S
dalem38.h H = c ˙ Q ˙ d ˙ T
dalem38.i I = c ˙ R ˙ d ˙ U
Assertion dalem41 φ Y = Z ψ G H

Proof

Step Hyp Ref Expression
1 dalem.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
2 dalem.l ˙ = K
3 dalem.j ˙ = join K
4 dalem.a A = Atoms K
5 dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
6 dalem38.m ˙ = meet K
7 dalem38.o O = LPlanes K
8 dalem38.y Y = P ˙ Q ˙ R
9 dalem38.z Z = S ˙ T ˙ U
10 dalem38.g G = c ˙ P ˙ d ˙ S
11 dalem38.h H = c ˙ Q ˙ d ˙ T
12 dalem38.i I = c ˙ R ˙ d ˙ U
13 1 dalemkehl φ K HL
14 13 3ad2ant1 φ Y = Z ψ K HL
15 1 2 3 4 5 6 7 8 9 11 dalem29 φ Y = Z ψ H A
16 1 2 3 4 5 6 7 8 9 12 dalem34 φ Y = Z ψ I A
17 1 2 3 4 5 6 7 8 9 10 dalem23 φ Y = Z ψ G A
18 1 2 3 4 5 6 7 8 9 10 11 12 dalem39 φ Y = Z ψ ¬ H ˙ I ˙ G
19 2 3 4 atnlej2 K HL H A I A G A ¬ H ˙ I ˙ G H G
20 14 15 16 17 18 19 syl131anc φ Y = Z ψ H G
21 20 necomd φ Y = Z ψ G H