Metamath Proof Explorer


Theorem dalawlem14

Description: Lemma for dalaw . Combine dalawlem10 and dalawlem13 . (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
dalawlem2.o O = LPlanes K
Assertion dalawlem14 K HL ¬ P ˙ Q ˙ R O ¬ 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 dalawlem2.o O = LPlanes K
6 ianor ¬ P ˙ Q ˙ R O ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P ¬ P ˙ Q ˙ R O ¬ ¬ P ˙ S ˙ Q ˙ T ˙ P ˙ Q ¬ P ˙ S ˙ Q ˙ T ˙ Q ˙ R ¬ P ˙ S ˙ Q ˙ T ˙ R ˙ P
7 1 2 3 4 5 dalawlem13 K HL ¬ P ˙ Q ˙ R O 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
8 7 3expib K HL ¬ P ˙ Q ˙ R O 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
9 8 3exp K HL ¬ P ˙ Q ˙ R O 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
10 1 2 3 4 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
11 10 3expib 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
12 11 3exp 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
13 9 12 jaod K HL ¬ P ˙ Q ˙ R O ¬ ¬ 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
14 6 13 syl5bi K HL ¬ P ˙ Q ˙ R O ¬ 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
15 14 3imp K HL ¬ P ˙ Q ˙ R O ¬ 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
16 15 3impib K HL ¬ P ˙ Q ˙ R O ¬ 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