Metamath Proof Explorer


Theorem dalemqrprot

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012)

Ref Expression
Hypotheses dalema.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
dalemb.j ˙ = join K
dalemb.a A = Atoms K
Assertion dalemqrprot φ Q ˙ R ˙ P = P ˙ Q ˙ R

Proof

Step Hyp Ref Expression
1 dalema.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 dalemb.j ˙ = join K
3 dalemb.a A = Atoms K
4 1 dalemkehl φ K HL
5 1 dalemqea φ Q A
6 1 dalemrea φ R A
7 1 dalempea φ P A
8 2 3 hlatjrot K HL Q A R A P A Q ˙ R ˙ P = P ˙ Q ˙ R
9 4 5 6 7 8 syl13anc φ Q ˙ R ˙ P = P ˙ Q ˙ R