Metamath Proof Explorer


Theorem 3atlem3

Description: Lemma for 3at . (Contributed by NM, 23-Jun-2012)

Ref Expression
Hypotheses 3at.l ˙ = K
3at.j ˙ = join K
3at.a A = Atoms K
Assertion 3atlem3 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U

Proof

Step Hyp Ref Expression
1 3at.l ˙ = K
2 3at.j ˙ = join K
3 3at.a A = Atoms K
4 simpl1 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U K HL P A Q A R A S A T A U A
5 simpl21 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U ¬ R ˙ P ˙ Q
6 simpl22 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U P U
7 simpr K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U P ˙ T ˙ U
8 6 7 jca K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U P U P ˙ T ˙ U
9 simpl23 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U ¬ Q ˙ P ˙ U
10 simpl3 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U
11 1 2 3 3atlem2 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U P ˙ T ˙ U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
12 4 5 8 9 10 11 syl131anc K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
13 simpl1 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ P ˙ T ˙ U K HL P A Q A R A S A T A U A
14 simpl21 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ P ˙ T ˙ U ¬ R ˙ P ˙ Q
15 simpr K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ P ˙ T ˙ U ¬ P ˙ T ˙ U
16 simpl23 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ P ˙ T ˙ U ¬ Q ˙ P ˙ U
17 simpl3 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ P ˙ T ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U
18 1 2 3 3atlem1 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q ¬ P ˙ T ˙ U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
19 13 14 15 16 17 18 syl131anc K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ P ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
20 12 19 pm2.61dan K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U