Metamath Proof Explorer


Theorem dalem62

Description: Lemma for dath . Eliminate the condition ps containing dummy variables c and d . (Contributed by NM, 11-Aug-2012)

Ref Expression
Hypotheses dalem62.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
dalem62.l ˙ = K
dalem62.j ˙ = join K
dalem62.a A = Atoms K
dalem62.m ˙ = meet K
dalem62.o O = LPlanes K
dalem62.y Y = P ˙ Q ˙ R
dalem62.z Z = S ˙ T ˙ U
dalem62.d D = P ˙ Q ˙ S ˙ T
dalem62.e E = Q ˙ R ˙ T ˙ U
dalem62.f F = R ˙ P ˙ U ˙ S
Assertion dalem62 φ Y = Z F ˙ D ˙ E

Proof

Step Hyp Ref Expression
1 dalem62.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 dalem62.l ˙ = K
3 dalem62.j ˙ = join K
4 dalem62.a A = Atoms K
5 dalem62.m ˙ = meet K
6 dalem62.o O = LPlanes K
7 dalem62.y Y = P ˙ Q ˙ R
8 dalem62.z Z = S ˙ T ˙ U
9 dalem62.d D = P ˙ Q ˙ S ˙ T
10 dalem62.e E = Q ˙ R ˙ T ˙ U
11 dalem62.f F = R ˙ P ˙ U ˙ S
12 biid c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
13 1 2 3 4 12 6 7 8 dalem20 φ Y = Z c d c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
14 1 2 3 4 12 5 6 7 8 9 10 11 dalem61 φ Y = Z c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d F ˙ D ˙ E
15 14 3expia φ Y = Z c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d F ˙ D ˙ E
16 15 exlimdvv φ Y = Z c d c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d F ˙ D ˙ E
17 13 16 mpd φ Y = Z F ˙ D ˙ E