Metamath Proof Explorer


Theorem 4atlem12

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

Ref Expression
Hypotheses 4at.l ˙=K
4at.j ˙=joinK
4at.a A=AtomsK
Assertion 4atlem12 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙Q˙R˙S˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W

Proof

Step Hyp Ref Expression
1 4at.l ˙=K
2 4at.j ˙=joinK
3 4at.a A=AtomsK
4 simpl11 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHL
5 4 hllatd KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKLat
6 simpl12 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RPA
7 eqid BaseK=BaseK
8 7 3 atbase PAPBaseK
9 6 8 syl KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RPBaseK
10 simpl13 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RQA
11 7 3 atbase QAQBaseK
12 10 11 syl KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RQBaseK
13 simpl23 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RTA
14 simpl31 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RUA
15 7 2 3 hlatjcl KHLTAUAT˙UBaseK
16 4 13 14 15 syl3anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RT˙UBaseK
17 simpl32 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RVA
18 simpl33 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RWA
19 7 2 3 hlatjcl KHLVAWAV˙WBaseK
20 4 17 18 19 syl3anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RV˙WBaseK
21 7 2 latjcl KLatT˙UBaseKV˙WBaseKT˙U˙V˙WBaseK
22 5 16 20 21 syl3anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RT˙U˙V˙WBaseK
23 7 1 2 latjle12 KLatPBaseKQBaseKT˙U˙V˙WBaseKP˙T˙U˙V˙WQ˙T˙U˙V˙WP˙Q˙T˙U˙V˙W
24 5 9 12 22 23 syl13anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WP˙Q˙T˙U˙V˙W
25 simpl21 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RRA
26 7 3 atbase RARBaseK
27 25 26 syl KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RRBaseK
28 simpl22 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RSA
29 7 3 atbase SASBaseK
30 28 29 syl KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RSBaseK
31 7 1 2 latjle12 KLatRBaseKSBaseKT˙U˙V˙WBaseKR˙T˙U˙V˙WS˙T˙U˙V˙WR˙S˙T˙U˙V˙W
32 5 27 30 22 31 syl13anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RR˙T˙U˙V˙WS˙T˙U˙V˙WR˙S˙T˙U˙V˙W
33 24 32 anbi12d KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙T˙U˙V˙WR˙S˙T˙U˙V˙W
34 simpl1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHLPAQA
35 7 2 3 hlatjcl KHLPAQAP˙QBaseK
36 34 35 syl KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙QBaseK
37 7 2 3 hlatjcl KHLRASAR˙SBaseK
38 4 25 28 37 syl3anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RR˙SBaseK
39 7 1 2 latjle12 KLatP˙QBaseKR˙SBaseKT˙U˙V˙WBaseKP˙Q˙T˙U˙V˙WR˙S˙T˙U˙V˙WP˙Q˙R˙S˙T˙U˙V˙W
40 5 36 38 22 39 syl13anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙Q˙T˙U˙V˙WR˙S˙T˙U˙V˙WP˙Q˙R˙S˙T˙U˙V˙W
41 33 40 bitrd KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S˙T˙U˙V˙W
42 simp1l KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WKHLPAQARASATAUAVAWA
43 simp1r KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WPQ¬R˙P˙Q¬S˙P˙Q˙R
44 simp2 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙W¬P˙U˙V˙W
45 simp3 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙W
46 1 2 3 4atlem12b KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
47 42 43 44 45 46 syl121anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
48 47 3exp KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
49 7 2 latj4rot KLatQBaseKRBaseKSBaseKPBaseKQ˙R˙S˙P=P˙Q˙R˙S
50 5 12 27 30 9 49 syl122anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RQ˙R˙S˙P=P˙Q˙R˙S
51 50 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WQ˙R˙S˙P=P˙Q˙R˙S
52 4 10 25 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHLQARA
53 28 6 13 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RSAPATA
54 simpl3 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RUAVAWA
55 52 53 54 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHLQARASAPATAUAVAWA
56 55 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WKHLQARASAPATAUAVAWA
57 simpr KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RPQ¬R˙P˙Q¬S˙P˙Q˙R
58 1 2 3 4noncolr3 KHLPAQARASAPQ¬R˙P˙Q¬S˙P˙Q˙RQR¬S˙Q˙R¬P˙Q˙R˙S
59 34 25 28 57 58 syl121anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RQR¬S˙Q˙R¬P˙Q˙R˙S
60 59 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WQR¬S˙Q˙R¬P˙Q˙R˙S
61 simp2 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙W¬Q˙U˙V˙W
62 simprlr KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WQ˙T˙U˙V˙W
63 simprrl KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WR˙T˙U˙V˙W
64 62 63 jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙W
65 simprrr KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WS˙T˙U˙V˙W
66 simprll KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙W
67 64 65 66 jca32 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙W
68 67 3adant2 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙W
69 1 2 3 4atlem12b KHLQARASAPATAUAVAWAQR¬S˙Q˙R¬P˙Q˙R˙S¬Q˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙R˙S˙P=T˙U˙V˙W
70 56 60 61 68 69 syl121anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WQ˙R˙S˙P=T˙U˙V˙W
71 51 70 eqtr3d KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
72 71 3exp KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
73 48 72 jaod KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙W¬Q˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
74 7 2 latjcom KLatP˙QBaseKR˙SBaseKP˙Q˙R˙S=R˙S˙P˙Q
75 5 36 38 74 syl3anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙Q˙R˙S=R˙S˙P˙Q
76 75 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=R˙S˙P˙Q
77 4 25 28 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHLRASA
78 6 10 13 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RPAQATA
79 77 78 54 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHLRASAPAQATAUAVAWA
80 79 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WKHLRASAPAQATAUAVAWA
81 1 2 3 4noncolr2 KHLPAQARASAPQ¬R˙P˙Q¬S˙P˙Q˙RRS¬P˙R˙S¬Q˙R˙S˙P
82 34 25 28 57 81 syl121anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RRS¬P˙R˙S¬Q˙R˙S˙P
83 82 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WRS¬P˙R˙S¬Q˙R˙S˙P
84 simp2 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙W¬R˙U˙V˙W
85 simprr KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙W
86 simprl KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙W
87 85 86 jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙W
88 87 3adant2 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙W
89 1 2 3 4atlem12b KHLRASAPAQATAUAVAWARS¬P˙R˙S¬Q˙R˙S˙P¬R˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙S˙P˙Q=T˙U˙V˙W
90 80 83 84 88 89 syl121anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WR˙S˙P˙Q=T˙U˙V˙W
91 76 90 eqtrd KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
92 91 3exp KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
93 7 2 latj4rot KLatPBaseKQBaseKRBaseKSBaseKP˙Q˙R˙S=S˙P˙Q˙R
94 5 9 12 27 30 93 syl122anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙Q˙R˙S=S˙P˙Q˙R
95 94 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=S˙P˙Q˙R
96 4 28 6 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHLSAPA
97 10 25 13 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RQARATA
98 96 97 54 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RKHLSAPAQARATAUAVAWA
99 98 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WKHLSAPAQARATAUAVAWA
100 1 2 3 4noncolr1 KHLPAQARASAPQ¬R˙P˙Q¬S˙P˙Q˙RSP¬Q˙S˙P¬R˙S˙P˙Q
101 34 25 28 57 100 syl121anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RSP¬Q˙S˙P¬R˙S˙P˙Q
102 101 3ad2ant1 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WSP¬Q˙S˙P¬R˙S˙P˙Q
103 simp2 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙W¬S˙U˙V˙W
104 65 66 jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙W
105 104 62 63 jca32 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙W
106 105 3adant2 KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙W
107 1 2 3 4atlem12b KHLSAPAQARATAUAVAWASP¬Q˙S˙P¬R˙S˙P˙Q¬S˙U˙V˙WS˙T˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙P˙Q˙R=T˙U˙V˙W
108 99 102 103 106 107 syl121anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WS˙P˙Q˙R=T˙U˙V˙W
109 95 108 eqtrd KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
110 109 3exp KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
111 92 110 jaod KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬R˙U˙V˙W¬S˙U˙V˙WP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
112 25 28 14 3jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RRASAUA
113 17 18 jca KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RVAWA
114 1 2 3 4atlem3 KHLPAQARASAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙W¬Q˙U˙V˙W¬R˙U˙V˙W¬S˙U˙V˙W
115 34 112 113 57 114 syl31anc KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙R¬P˙U˙V˙W¬Q˙U˙V˙W¬R˙U˙V˙W¬S˙U˙V˙W
116 73 111 115 mpjaod KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙T˙U˙V˙WQ˙T˙U˙V˙WR˙T˙U˙V˙WS˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W
117 41 116 sylbird KHLPAQARASATAUAVAWAPQ¬R˙P˙Q¬S˙P˙Q˙RP˙Q˙R˙S˙T˙U˙V˙WP˙Q˙R˙S=T˙U˙V˙W