Metamath Proof Explorer


Theorem dalawlem10

Description: Lemma for dalaw . Combine dalawlem5 , dalawlem8 , and dalawlem9 . (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l ˙ = K
dalawlem.j ˙ = join K
dalawlem.m ˙ = meet K
dalawlem.a A = Atoms K
Assertion dalawlem10 K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S

Proof

Step Hyp Ref Expression
1 dalawlem.l ˙ = K
2 dalawlem.j ˙ = join K
3 dalawlem.m ˙ = meet K
4 dalawlem.a A = Atoms K
5 simp11 K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A K HL
6 simp12 K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P
7 3oran P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ P ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P
8 6 7 sylibr K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ P
9 simp13 K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U
10 simp2 K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P A Q A R A
11 simp3 K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S A T A U A
12 1 2 3 4 dalawlem5 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
13 12 3expib K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
14 13 3exp K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
15 1 2 3 4 dalawlem8 K HL P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
16 15 3expib K HL P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
17 16 3exp K HL P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
18 1 2 3 4 dalawlem9 K HL P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
19 18 3expib K HL P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
20 19 3exp K HL P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
21 14 17 20 3jaod K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
22 21 3imp K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
23 22 3impib K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
24 5 8 9 10 11 23 syl311anc K HL ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S