Metamath Proof Explorer

Theorem mdsymlem5

Description: Lemma for mdsymi . (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 
|- A e. CH
mdsymlem1.2 
|- B e. CH
mdsymlem1.3 
|- C = ( A vH p )
Assertion mdsymlem5 
|- ( ( q e. HAtoms /\ r e. HAtoms ) -> ( -. q = p -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 
 |-  A e. CH
2 mdsymlem1.2 
 |-  B e. CH
3 mdsymlem1.3 
 |-  C = ( A vH p )
4 df-ne 
 |-  ( q =/= p <-> -. q = p )
5 atnemeq0 
 |-  ( ( q e. HAtoms /\ p e. HAtoms ) -> ( q =/= p <-> ( q i^i p ) = 0H ) )
6 4 5 bitr3id 
 |-  ( ( q e. HAtoms /\ p e. HAtoms ) -> ( -. q = p <-> ( q i^i p ) = 0H ) )
7 6 anbi2d 
 |-  ( ( q e. HAtoms /\ p e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ -. q = p ) <-> ( p C_ ( q vH r ) /\ ( q i^i p ) = 0H ) ) )
8 7 3adant3 
 |-  ( ( q e. HAtoms /\ p e. HAtoms /\ r e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ -. q = p ) <-> ( p C_ ( q vH r ) /\ ( q i^i p ) = 0H ) ) )
9 atelch 
 |-  ( q e. HAtoms -> q e. CH )
10 atexch 
 |-  ( ( q e. CH /\ p e. HAtoms /\ r e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ ( q i^i p ) = 0H ) -> r C_ ( q vH p ) ) )
11 9 10 syl3an1 
 |-  ( ( q e. HAtoms /\ p e. HAtoms /\ r e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ ( q i^i p ) = 0H ) -> r C_ ( q vH p ) ) )
12 8 11 sylbid 
 |-  ( ( q e. HAtoms /\ p e. HAtoms /\ r e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ -. q = p ) -> r C_ ( q vH p ) ) )
13 12 expd 
 |-  ( ( q e. HAtoms /\ p e. HAtoms /\ r e. HAtoms ) -> ( p C_ ( q vH r ) -> ( -. q = p -> r C_ ( q vH p ) ) ) )
14 13 3com23 
 |-  ( ( q e. HAtoms /\ r e. HAtoms /\ p e. HAtoms ) -> ( p C_ ( q vH r ) -> ( -. q = p -> r C_ ( q vH p ) ) ) )
15 14 3expa 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ p e. HAtoms ) -> ( p C_ ( q vH r ) -> ( -. q = p -> r C_ ( q vH p ) ) ) )
16 15 adantrl 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) -> ( p C_ ( q vH r ) -> ( -. q = p -> r C_ ( q vH p ) ) ) )
17 16 adantrd 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( -. q = p -> r C_ ( q vH p ) ) ) )
18 17 imp32 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) -> r C_ ( q vH p ) )
19 18 adantrl 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) ) -> r C_ ( q vH p ) )
20 19 adantrr 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) ) -> r C_ ( q vH p ) )
21 simplrl 
 |-  ( ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) -> q C_ A )
22 atelch 
 |-  ( p e. HAtoms -> p e. CH )
23 22 anim1i 
 |-  ( ( p e. HAtoms /\ c e. CH ) -> ( p e. CH /\ c e. CH ) )
24 23 ancoms 
 |-  ( ( c e. CH /\ p e. HAtoms ) -> ( p e. CH /\ c e. CH ) )
25 chub2 
 |-  ( ( A e. CH /\ c e. CH ) -> A C_ ( c vH A ) )
26 1 25 mpan 
 |-  ( c e. CH -> A C_ ( c vH A ) )
27 sstr 
 |-  ( ( q C_ A /\ A C_ ( c vH A ) ) -> q C_ ( c vH A ) )
28 26 27 sylan2 
 |-  ( ( q C_ A /\ c e. CH ) -> q C_ ( c vH A ) )
29 chub1 
 |-  ( ( c e. CH /\ A e. CH ) -> c C_ ( c vH A ) )
30 1 29 mpan2 
 |-  ( c e. CH -> c C_ ( c vH A ) )
31 sstr 
 |-  ( ( p C_ c /\ c C_ ( c vH A ) ) -> p C_ ( c vH A ) )
32 30 31 sylan2 
 |-  ( ( p C_ c /\ c e. CH ) -> p C_ ( c vH A ) )
33 28 32 anim12i 
 |-  ( ( ( q C_ A /\ c e. CH ) /\ ( p C_ c /\ c e. CH ) ) -> ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) )
34 33 anandirs 
 |-  ( ( ( q C_ A /\ p C_ c ) /\ c e. CH ) -> ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) )
35 34 ancoms 
 |-  ( ( c e. CH /\ ( q C_ A /\ p C_ c ) ) -> ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) )
36 35 adantll 
 |-  ( ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) /\ ( q C_ A /\ p C_ c ) ) -> ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) )
37 chjcl 
 |-  ( ( c e. CH /\ A e. CH ) -> ( c vH A ) e. CH )
38 1 37 mpan2 
 |-  ( c e. CH -> ( c vH A ) e. CH )
39 chlub 
 |-  ( ( q e. CH /\ p e. CH /\ ( c vH A ) e. CH ) -> ( ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) <-> ( q vH p ) C_ ( c vH A ) ) )
40 38 39 syl3an3 
 |-  ( ( q e. CH /\ p e. CH /\ c e. CH ) -> ( ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) <-> ( q vH p ) C_ ( c vH A ) ) )
41 40 3expa 
 |-  ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) -> ( ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) <-> ( q vH p ) C_ ( c vH A ) ) )
42 41 adantr 
 |-  ( ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) /\ ( q C_ A /\ p C_ c ) ) -> ( ( q C_ ( c vH A ) /\ p C_ ( c vH A ) ) <-> ( q vH p ) C_ ( c vH A ) ) )
43 36 42 mpbid 
 |-  ( ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) /\ ( q C_ A /\ p C_ c ) ) -> ( q vH p ) C_ ( c vH A ) )
44 43 adantrl 
 |-  ( ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) /\ ( A C_ c /\ ( q C_ A /\ p C_ c ) ) ) -> ( q vH p ) C_ ( c vH A ) )
45 chlejb2 
 |-  ( ( A e. CH /\ c e. CH ) -> ( A C_ c <-> ( c vH A ) = c ) )
46 1 45 mpan 
 |-  ( c e. CH -> ( A C_ c <-> ( c vH A ) = c ) )
47 46 biimpa 
 |-  ( ( c e. CH /\ A C_ c ) -> ( c vH A ) = c )
48 47 ad2ant2lr 
 |-  ( ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) /\ ( A C_ c /\ ( q C_ A /\ p C_ c ) ) ) -> ( c vH A ) = c )
49 44 48 sseqtrd 
 |-  ( ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) /\ ( A C_ c /\ ( q C_ A /\ p C_ c ) ) ) -> ( q vH p ) C_ c )
50 49 exp45 
 |-  ( ( ( q e. CH /\ p e. CH ) /\ c e. CH ) -> ( A C_ c -> ( q C_ A -> ( p C_ c -> ( q vH p ) C_ c ) ) ) )
51 50 anasss 
 |-  ( ( q e. CH /\ ( p e. CH /\ c e. CH ) ) -> ( A C_ c -> ( q C_ A -> ( p C_ c -> ( q vH p ) C_ c ) ) ) )
52 9 24 51 syl2an 
 |-  ( ( q e. HAtoms /\ ( c e. CH /\ p e. HAtoms ) ) -> ( A C_ c -> ( q C_ A -> ( p C_ c -> ( q vH p ) C_ c ) ) ) )
53 52 adantlr 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) -> ( A C_ c -> ( q C_ A -> ( p C_ c -> ( q vH p ) C_ c ) ) ) )
54 21 53 syl7 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) -> ( A C_ c -> ( ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) -> ( p C_ c -> ( q vH p ) C_ c ) ) ) )
55 54 imp44 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) ) -> ( q vH p ) C_ c )
56 20 55 sstrd 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) ) -> r C_ c )
57 simplrr 
 |-  ( ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) -> r C_ B )
58 57 ad2antlr 
 |-  ( ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) -> r C_ B )
59 58 adantl 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) ) -> r C_ B )
60 56 59 ssind 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) ) -> r C_ ( c i^i B ) )
61 atelch 
 |-  ( r e. HAtoms -> r e. CH )
62 9 61 anim12i 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( q e. CH /\ r e. CH ) )
63 chincl 
 |-  ( ( c e. CH /\ B e. CH ) -> ( c i^i B ) e. CH )
64 2 63 mpan2 
 |-  ( c e. CH -> ( c i^i B ) e. CH )
65 chlej1 
 |-  ( ( ( r e. CH /\ ( c i^i B ) e. CH /\ q e. CH ) /\ r C_ ( c i^i B ) ) -> ( r vH q ) C_ ( ( c i^i B ) vH q ) )
66 65 ex 
 |-  ( ( r e. CH /\ ( c i^i B ) e. CH /\ q e. CH ) -> ( r C_ ( c i^i B ) -> ( r vH q ) C_ ( ( c i^i B ) vH q ) ) )
67 64 66 syl3an2 
 |-  ( ( r e. CH /\ c e. CH /\ q e. CH ) -> ( r C_ ( c i^i B ) -> ( r vH q ) C_ ( ( c i^i B ) vH q ) ) )
68 67 3comr 
 |-  ( ( q e. CH /\ r e. CH /\ c e. CH ) -> ( r C_ ( c i^i B ) -> ( r vH q ) C_ ( ( c i^i B ) vH q ) ) )
69 68 3expa 
 |-  ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) -> ( r C_ ( c i^i B ) -> ( r vH q ) C_ ( ( c i^i B ) vH q ) ) )
70 69 adantr 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ q C_ A ) -> ( r C_ ( c i^i B ) -> ( r vH q ) C_ ( ( c i^i B ) vH q ) ) )
71 chlej2 
 |-  ( ( ( q e. CH /\ A e. CH /\ ( c i^i B ) e. CH ) /\ q C_ A ) -> ( ( c i^i B ) vH q ) C_ ( ( c i^i B ) vH A ) )
72 1 71 mp3anl2 
 |-  ( ( ( q e. CH /\ ( c i^i B ) e. CH ) /\ q C_ A ) -> ( ( c i^i B ) vH q ) C_ ( ( c i^i B ) vH A ) )
73 64 72 sylanl2 
 |-  ( ( ( q e. CH /\ c e. CH ) /\ q C_ A ) -> ( ( c i^i B ) vH q ) C_ ( ( c i^i B ) vH A ) )
74 73 adantllr 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ q C_ A ) -> ( ( c i^i B ) vH q ) C_ ( ( c i^i B ) vH A ) )
75 sstr2 
 |-  ( ( r vH q ) C_ ( ( c i^i B ) vH q ) -> ( ( ( c i^i B ) vH q ) C_ ( ( c i^i B ) vH A ) -> ( r vH q ) C_ ( ( c i^i B ) vH A ) ) )
76 74 75 syl5com 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ q C_ A ) -> ( ( r vH q ) C_ ( ( c i^i B ) vH q ) -> ( r vH q ) C_ ( ( c i^i B ) vH A ) ) )
77 chjcom 
 |-  ( ( q e. CH /\ r e. CH ) -> ( q vH r ) = ( r vH q ) )
78 77 ad2antrr 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ q C_ A ) -> ( q vH r ) = ( r vH q ) )
79 78 sseq1d 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ q C_ A ) -> ( ( q vH r ) C_ ( ( c i^i B ) vH A ) <-> ( r vH q ) C_ ( ( c i^i B ) vH A ) ) )
80 76 79 sylibrd 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ q C_ A ) -> ( ( r vH q ) C_ ( ( c i^i B ) vH q ) -> ( q vH r ) C_ ( ( c i^i B ) vH A ) ) )
81 70 80 syld 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ q C_ A ) -> ( r C_ ( c i^i B ) -> ( q vH r ) C_ ( ( c i^i B ) vH A ) ) )
82 81 adantrl 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ ( p C_ ( q vH r ) /\ q C_ A ) ) -> ( r C_ ( c i^i B ) -> ( q vH r ) C_ ( ( c i^i B ) vH A ) ) )
83 sstr2 
 |-  ( p C_ ( q vH r ) -> ( ( q vH r ) C_ ( ( c i^i B ) vH A ) -> p C_ ( ( c i^i B ) vH A ) ) )
84 83 ad2antrl 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ ( p C_ ( q vH r ) /\ q C_ A ) ) -> ( ( q vH r ) C_ ( ( c i^i B ) vH A ) -> p C_ ( ( c i^i B ) vH A ) ) )
85 82 84 syld 
 |-  ( ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) /\ ( p C_ ( q vH r ) /\ q C_ A ) ) -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) )
86 85 exp32 
 |-  ( ( ( q e. CH /\ r e. CH ) /\ c e. CH ) -> ( p C_ ( q vH r ) -> ( q C_ A -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) ) ) )
87 62 86 sylan 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ c e. CH ) -> ( p C_ ( q vH r ) -> ( q C_ A -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) ) ) )
88 87 adantrr 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) -> ( p C_ ( q vH r ) -> ( q C_ A -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) ) ) )
89 88 imp31 
 |-  ( ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ p C_ ( q vH r ) ) /\ q C_ A ) -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) )
90 89 adantrr 
 |-  ( ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ p C_ ( q vH r ) ) /\ ( q C_ A /\ r C_ B ) ) -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) )
91 90 anasss 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) )
92 91 adantrr 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) )
93 92 adantrl 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) ) -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) )
94 93 adantrr 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) ) -> ( r C_ ( c i^i B ) -> p C_ ( ( c i^i B ) vH A ) ) )
95 60 94 mpd 
 |-  ( ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) /\ ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) /\ p C_ c ) ) -> p C_ ( ( c i^i B ) vH A ) )
96 95 exp32 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) -> ( ( A C_ c /\ ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ -. q = p ) ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
97 96 exp4d 
 |-  ( ( ( q e. HAtoms /\ r e. HAtoms ) /\ ( c e. CH /\ p e. HAtoms ) ) -> ( A C_ c -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( -. q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) )
98 97 exp32 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( c e. CH -> ( p e. HAtoms -> ( A C_ c -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( -. q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) ) ) )
99 98 com34 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( c e. CH -> ( A C_ c -> ( p e. HAtoms -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( -. q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) ) ) )
100 99 imp4c 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( -. q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) )
101 100 com24 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( -. q = p -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) )