Metamath Proof Explorer


Theorem dalempjqeb

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 dalempjqeb φ P ˙ Q Base K

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 dalempea φ P A
6 1 dalemqea φ Q A
7 eqid Base K = Base K
8 7 2 3 hlatjcl K HL P A Q A P ˙ Q Base K
9 4 5 6 8 syl3anc φ P ˙ Q Base K