Metamath Proof Explorer


Theorem 4atlem11

Description: Lemma for 4at . Combine all three possible cases. (Contributed by NM, 10-Jul-2012)

Ref Expression
Hypotheses 4at.l ˙ = K
4at.j ˙ = join K
4at.a A = Atoms K
Assertion 4atlem11 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ R ˙ S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W

Proof

Step Hyp Ref Expression
1 4at.l ˙ = K
2 4at.j ˙ = join K
3 4at.a A = Atoms K
4 3anass Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W
5 simpl11 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R K HL
6 5 hllatd K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R K Lat
7 simpl2l K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R R A
8 eqid Base K = Base K
9 8 3 atbase R A R Base K
10 7 9 syl K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R R Base K
11 simpl2r K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S A
12 8 3 atbase S A S Base K
13 11 12 syl K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S Base K
14 simpl12 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P A
15 simpl31 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R U A
16 8 2 3 hlatjcl K HL P A U A P ˙ U Base K
17 5 14 15 16 syl3anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P ˙ U Base K
18 simpl32 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R V A
19 simpl33 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R W A
20 8 2 3 hlatjcl K HL V A W A V ˙ W Base K
21 5 18 19 20 syl3anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R V ˙ W Base K
22 8 2 latjcl K Lat P ˙ U Base K V ˙ W Base K P ˙ U ˙ V ˙ W Base K
23 6 17 21 22 syl3anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P ˙ U ˙ V ˙ W Base K
24 8 1 2 latjle12 K Lat R Base K S Base K P ˙ U ˙ V ˙ W Base K R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W R ˙ S ˙ P ˙ U ˙ V ˙ W
25 6 10 13 23 24 syl13anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W R ˙ S ˙ P ˙ U ˙ V ˙ W
26 25 anbi2d K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ S ˙ P ˙ U ˙ V ˙ W
27 4 26 syl5bb K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ S ˙ P ˙ U ˙ V ˙ W
28 simpl13 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q A
29 8 3 atbase Q A Q Base K
30 28 29 syl K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q Base K
31 8 2 3 hlatjcl K HL R A S A R ˙ S Base K
32 5 7 11 31 syl3anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R R ˙ S Base K
33 8 1 2 latjle12 K Lat Q Base K R ˙ S Base K P ˙ U ˙ V ˙ W Base K Q ˙ P ˙ U ˙ V ˙ W R ˙ S ˙ P ˙ U ˙ V ˙ W Q ˙ R ˙ S ˙ P ˙ U ˙ V ˙ W
34 6 30 32 23 33 syl13anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ S ˙ P ˙ U ˙ V ˙ W Q ˙ R ˙ S ˙ P ˙ U ˙ V ˙ W
35 27 34 bitrd K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ R ˙ S ˙ P ˙ U ˙ V ˙ W
36 simpl1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R K HL P A Q A
37 simpl2 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R R A S A
38 18 19 jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R V A W A
39 simpr K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R
40 1 2 3 4atlem3a K HL P A Q A R A S A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W ¬ R ˙ P ˙ V ˙ W ¬ S ˙ P ˙ V ˙ W
41 36 37 38 39 40 syl31anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W ¬ R ˙ P ˙ V ˙ W ¬ S ˙ P ˙ V ˙ W
42 simp1l K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W K HL P A Q A R A S A U A V A W A
43 simp1r K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R
44 simp2 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W ¬ Q ˙ P ˙ V ˙ W
45 simp3 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W
46 1 2 3 4atlem11b K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
47 42 43 44 45 46 syl121anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
48 47 3exp K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
49 5 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W K HL
50 14 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P A
51 28 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q A
52 7 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W R A
53 11 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W S A
54 2 3 hlatj4 K HL P A Q A R A S A P ˙ Q ˙ R ˙ S = P ˙ R ˙ Q ˙ S
55 49 50 51 52 53 54 syl122anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ R ˙ Q ˙ S
56 49 50 52 3jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W K HL P A R A
57 51 53 jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q A S A
58 simp1l3 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W U A V A W A
59 simp1r2 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W ¬ R ˙ P ˙ Q
60 1 2 3 4atlem0be K HL P A Q A R A ¬ R ˙ P ˙ Q P R
61 49 50 51 52 59 60 syl131anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P R
62 simp1r1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P Q
63 1 2 3 4atlem0ae K HL P A Q A R A P Q ¬ R ˙ P ˙ Q ¬ Q ˙ P ˙ R
64 49 50 51 52 62 59 63 syl132anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W ¬ Q ˙ P ˙ R
65 simp1r3 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W ¬ S ˙ P ˙ Q ˙ R
66 2 3 hlatj32 K HL P A Q A R A P ˙ Q ˙ R = P ˙ R ˙ Q
67 49 50 51 52 66 syl13anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R = P ˙ R ˙ Q
68 67 breq2d K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ Q ˙ R S ˙ P ˙ R ˙ Q
69 65 68 mtbid K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W ¬ S ˙ P ˙ R ˙ Q
70 61 64 69 3jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P R ¬ Q ˙ P ˙ R ¬ S ˙ P ˙ R ˙ Q
71 simp2 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W ¬ R ˙ P ˙ V ˙ W
72 simp32 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W
73 simp31 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W
74 simp33 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W
75 1 2 3 4atlem11b K HL P A R A Q A S A U A V A W A P R ¬ Q ˙ P ˙ R ¬ S ˙ P ˙ R ˙ Q ¬ R ˙ P ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ R ˙ Q ˙ S = P ˙ U ˙ V ˙ W
76 56 57 58 70 71 72 73 74 75 syl323anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ R ˙ Q ˙ S = P ˙ U ˙ V ˙ W
77 55 76 eqtrd K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
78 77 3exp K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
79 8 3 atbase P A P Base K
80 14 79 syl K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P Base K
81 8 2 latj4rot K Lat P Base K Q Base K R Base K S Base K P ˙ Q ˙ R ˙ S = S ˙ P ˙ Q ˙ R
82 6 80 30 10 13 81 syl122anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S = S ˙ P ˙ Q ˙ R
83 2 3 hlatjcom K HL S A P A S ˙ P = P ˙ S
84 5 11 14 83 syl3anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S ˙ P = P ˙ S
85 84 oveq1d K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S ˙ P ˙ Q ˙ R = P ˙ S ˙ Q ˙ R
86 82 85 eqtrd K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S = P ˙ S ˙ Q ˙ R
87 86 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ S ˙ Q ˙ R
88 5 14 11 3jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R K HL P A S A
89 28 7 jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q A R A
90 simpl3 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R U A V A W A
91 88 89 90 3jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R K HL P A S A Q A R A U A V A W A
92 91 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W K HL P A S A Q A R A U A V A W A
93 1 2 3 4noncolr1 K HL P A Q A R A S A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S P ¬ Q ˙ S ˙ P ¬ R ˙ S ˙ P ˙ Q
94 36 37 39 93 syl3anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S P ¬ Q ˙ S ˙ P ¬ R ˙ S ˙ P ˙ Q
95 necom S P P S
96 95 a1i K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S P P S
97 84 breq2d K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ S ˙ P Q ˙ P ˙ S
98 97 notbid K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ S ˙ P ¬ Q ˙ P ˙ S
99 84 oveq1d K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S ˙ P ˙ Q = P ˙ S ˙ Q
100 99 breq2d K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R R ˙ S ˙ P ˙ Q R ˙ P ˙ S ˙ Q
101 100 notbid K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ R ˙ S ˙ P ˙ Q ¬ R ˙ P ˙ S ˙ Q
102 96 98 101 3anbi123d K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R S P ¬ Q ˙ S ˙ P ¬ R ˙ S ˙ P ˙ Q P S ¬ Q ˙ P ˙ S ¬ R ˙ P ˙ S ˙ Q
103 94 102 mpbid K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R P S ¬ Q ˙ P ˙ S ¬ R ˙ P ˙ S ˙ Q
104 103 3ad2ant1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P S ¬ Q ˙ P ˙ S ¬ R ˙ P ˙ S ˙ Q
105 simp2 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W ¬ S ˙ P ˙ V ˙ W
106 simpr3 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W
107 simpr1 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W
108 simpr2 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W
109 106 107 108 3jca K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W
110 109 3adant2 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W
111 1 2 3 4atlem11b K HL P A S A Q A R A U A V A W A P S ¬ Q ˙ P ˙ S ¬ R ˙ P ˙ S ˙ Q ¬ S ˙ P ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W P ˙ S ˙ Q ˙ R = P ˙ U ˙ V ˙ W
112 92 104 105 110 111 syl121anc K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ S ˙ Q ˙ R = P ˙ U ˙ V ˙ W
113 87 112 eqtrd K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
114 113 3exp K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
115 48 78 114 3jaod K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ Q ˙ P ˙ V ˙ W ¬ R ˙ P ˙ V ˙ W ¬ S ˙ P ˙ V ˙ W Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
116 41 115 mpd K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ P ˙ U ˙ V ˙ W R ˙ P ˙ U ˙ V ˙ W S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
117 35 116 sylbird K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ R ˙ S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W