Theorem nadddilem1

Description: Lemma for nadddi . Prove a subcase of the reverse implication. (Contributed by Scott Fenton, 31-Jul-2026)

	Ref	Expression
Hypotheses	nadddilem1.1	$$⊢\phi \to A\in \mathrm{On}$$
	nadddilem1.2	$$⊢\phi \to B\in \mathrm{On}$$
	nadddilem1.3	$$⊢\phi \to C\in \mathrm{On}$$
	nadddilem1.4	No typesetting found for |- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
	nadddilem1.5	No typesetting found for |- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) with typecode |-
	nadddilem1.6	No typesetting found for |- ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) with typecode |-
Assertion	nadddilem1	Could not format assertion : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nadddilem1.1	$$⊢\phi \to A\in \mathrm{On}$$
2		nadddilem1.2	$$⊢\phi \to B\in \mathrm{On}$$
3		nadddilem1.3	$$⊢\phi \to C\in \mathrm{On}$$
4		nadddilem1.4	Could not format ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) : No typesetting found for |- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
5		nadddilem1.5	Could not format ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) : No typesetting found for |- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) with typecode |-
6		nadddilem1.6	Could not format ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) : No typesetting found for |- ( ph -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) with typecode |-
7	1	adantr	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> A e. On ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> A e. On ) with typecode |-
8	3	adantr	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> C e. On ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> C e. On ) with typecode |-
9	7 8	nmulcld	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> ( A .no C ) e. On ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> ( A .no C ) e. On ) with typecode |-
10		simpr	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> Y e. ( A .no C ) ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> Y e. ( A .no C ) ) with typecode |-
11	9 10	onelond	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> Y e. On ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> Y e. On ) with typecode |-
12		ltnmul	Could not format ( ( Y e. On /\ A e. On /\ C e. On ) -> ( Y e. ( A .no C ) <-> E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) : No typesetting found for |- ( ( Y e. On /\ A e. On /\ C e. On ) -> ( Y e. ( A .no C ) <-> E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) with typecode |-
13	11 7 8 12	syl3anc	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> ( Y e. ( A .no C ) <-> E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> ( Y e. ( A .no C ) <-> E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) with typecode |-
14	1	ad2antrr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A e. On ) with typecode |-
15	2	ad2antrr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> B e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> B e. On ) with typecode |-
16	14 15	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no B ) e. On ) with typecode |-
17	11	adantr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> Y e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> Y e. On ) with typecode |-
18		simprll	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> z e. A ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> z e. A ) with typecode |-
19	14 18	onelond	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> z e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> z e. On ) with typecode |-
20	3	ad2antrr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> C e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> C e. On ) with typecode |-
21		simprlr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> w e. C ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> w e. C ) with typecode |-
22	20 21	onelond	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> w e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> w e. On ) with typecode |-
23	19 22	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no w ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no w ) e. On ) with typecode |-
24	16 17 23	naddassd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) = ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) = ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) ) with typecode |-
25	17 23	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( Y +no ( z .no w ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( Y +no ( z .no w ) ) e. On ) with typecode |-
26	16 25	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) e. On ) with typecode |-
27	15 20	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no C ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no C ) e. On ) with typecode |-
28	14 27	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no C ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no C ) ) e. On ) with typecode |-
29	28 23	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no C ) ) +no ( z .no w ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no C ) ) +no ( z .no w ) ) e. On ) with typecode |-
30		simprr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) with typecode |-
31	19 20	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no C ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no C ) e. On ) with typecode |-
32	14 22	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no w ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no w ) e. On ) with typecode |-
33	31 32	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no C ) +no ( A .no w ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no C ) +no ( A .no w ) ) e. On ) with typecode |-
34		naddss2	Could not format ( ( ( Y +no ( z .no w ) ) e. On /\ ( ( z .no C ) +no ( A .no w ) ) e. On /\ ( A .no B ) e. On ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) <-> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) ) : No typesetting found for |- ( ( ( Y +no ( z .no w ) ) e. On /\ ( ( z .no C ) +no ( A .no w ) ) e. On /\ ( A .no B ) e. On ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) <-> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) ) with typecode |-
35	25 33 16 34	syl3anc	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) <-> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) <-> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) ) with typecode |-
36	30 35	mpbid	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) C_ ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) with typecode |-
37		oveq2	$$⊢f=w\to B+f=B+w$$
38	37	oveq2d	Could not format ( f = w -> ( A .no ( B +no f ) ) = ( A .no ( B +no w ) ) ) : No typesetting found for |- ( f = w -> ( A .no ( B +no f ) ) = ( A .no ( B +no w ) ) ) with typecode |-
39		oveq2	Could not format ( f = w -> ( A .no f ) = ( A .no w ) ) : No typesetting found for |- ( f = w -> ( A .no f ) = ( A .no w ) ) with typecode |-
40	39	oveq2d	Could not format ( f = w -> ( ( A .no B ) +no ( A .no f ) ) = ( ( A .no B ) +no ( A .no w ) ) ) : No typesetting found for |- ( f = w -> ( ( A .no B ) +no ( A .no f ) ) = ( ( A .no B ) +no ( A .no w ) ) ) with typecode |-
41	38 40	eqeq12d	Could not format ( f = w -> ( ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> ( A .no ( B +no w ) ) = ( ( A .no B ) +no ( A .no w ) ) ) ) : No typesetting found for |- ( f = w -> ( ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) <-> ( A .no ( B +no w ) ) = ( ( A .no B ) +no ( A .no w ) ) ) ) with typecode |-
42	5	ad2antrr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) with typecode |-
43	41 42 21	rspcdva	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no w ) ) = ( ( A .no B ) +no ( A .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no w ) ) = ( ( A .no B ) +no ( A .no w ) ) ) with typecode |-
44	43	oveq1d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) = ( ( ( A .no B ) +no ( A .no w ) ) +no ( z .no C ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) = ( ( ( A .no B ) +no ( A .no w ) ) +no ( z .no C ) ) ) with typecode |-
45	16 32 31	nadd32d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no ( A .no w ) ) +no ( z .no C ) ) = ( ( ( A .no B ) +no ( z .no C ) ) +no ( A .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no ( A .no w ) ) +no ( z .no C ) ) = ( ( ( A .no B ) +no ( z .no C ) ) +no ( A .no w ) ) ) with typecode |-
46	16 31 32	naddassd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no ( z .no C ) ) +no ( A .no w ) ) = ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no ( z .no C ) ) +no ( A .no w ) ) = ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) ) with typecode |-
47	44 45 46	3eqtrrd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) = ( ( A .no ( B +no w ) ) +no ( z .no C ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) = ( ( A .no ( B +no w ) ) +no ( z .no C ) ) ) with typecode |-
48		naddel2	$$⊢\left(w\in \mathrm{On}\wedge C\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(w\in C\leftrightarrow B+w\in \left(B+C\right)\right)$$
49	22 20 15 48	syl3anc	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( w e. C <-> ( B +no w ) e. ( B +no C ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( w e. C <-> ( B +no w ) e. ( B +no C ) ) ) with typecode |-
50	21 49	mpbid	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no w ) e. ( B +no C ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no w ) e. ( B +no C ) ) with typecode |-
51		nmuladdel	Could not format ( ( ( A e. On /\ ( B +no C ) e. On ) /\ ( z e. A /\ ( B +no w ) e. ( B +no C ) ) ) -> ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ ( B +no C ) e. On ) /\ ( z e. A /\ ( B +no w ) e. ( B +no C ) ) ) -> ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) with typecode |-
52	14 27 18 50 51	syl22anc	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) with typecode |-
53	15 22	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no w ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( B +no w ) e. On ) with typecode |-
54	14 53	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no w ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( A .no ( B +no w ) ) e. On ) with typecode |-
55	19 15	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no B ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no B ) e. On ) with typecode |-
56	54 31 55	naddassd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( A .no ( B +no w ) ) +no ( ( z .no C ) +no ( z .no B ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( A .no ( B +no w ) ) +no ( ( z .no C ) +no ( z .no B ) ) ) ) with typecode |-
57		oveq1	Could not format ( d = z -> ( d .no ( B +no C ) ) = ( z .no ( B +no C ) ) ) : No typesetting found for |- ( d = z -> ( d .no ( B +no C ) ) = ( z .no ( B +no C ) ) ) with typecode |-
58		oveq1	Could not format ( d = z -> ( d .no B ) = ( z .no B ) ) : No typesetting found for |- ( d = z -> ( d .no B ) = ( z .no B ) ) with typecode |-
59		oveq1	Could not format ( d = z -> ( d .no C ) = ( z .no C ) ) : No typesetting found for |- ( d = z -> ( d .no C ) = ( z .no C ) ) with typecode |-
60	58 59	oveq12d	Could not format ( d = z -> ( ( d .no B ) +no ( d .no C ) ) = ( ( z .no B ) +no ( z .no C ) ) ) : No typesetting found for |- ( d = z -> ( ( d .no B ) +no ( d .no C ) ) = ( ( z .no B ) +no ( z .no C ) ) ) with typecode |-
61	57 60	eqeq12d	Could not format ( d = z -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( z .no ( B +no C ) ) = ( ( z .no B ) +no ( z .no C ) ) ) ) : No typesetting found for |- ( d = z -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( z .no ( B +no C ) ) = ( ( z .no B ) +no ( z .no C ) ) ) ) with typecode |-
62	4	ad2antrr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
63	61 62 18	rspcdva	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) = ( ( z .no B ) +no ( z .no C ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) = ( ( z .no B ) +no ( z .no C ) ) ) with typecode |-
64	55 31	naddcomd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no B ) +no ( z .no C ) ) = ( ( z .no C ) +no ( z .no B ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no B ) +no ( z .no C ) ) = ( ( z .no C ) +no ( z .no B ) ) ) with typecode |-
65	63 64	eqtrd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) = ( ( z .no C ) +no ( z .no B ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) = ( ( z .no C ) +no ( z .no B ) ) ) with typecode |-
66	65	oveq2d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) = ( ( A .no ( B +no w ) ) +no ( ( z .no C ) +no ( z .no B ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) = ( ( A .no ( B +no w ) ) +no ( ( z .no C ) +no ( z .no B ) ) ) ) with typecode |-
67	56 66	eqtr4d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) ) with typecode |-
68	19 27	nmulcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no C ) ) e. On ) with typecode |-
69	54 68	naddcomd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) = ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no ( B +no C ) ) ) = ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) ) with typecode |-
70	67 69	eqtrd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) = ( ( z .no ( B +no C ) ) +no ( A .no ( B +no w ) ) ) ) with typecode |-
71	28 23 55	naddassd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) = ( ( A .no ( B +no C ) ) +no ( ( z .no w ) +no ( z .no B ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) = ( ( A .no ( B +no C ) ) +no ( ( z .no w ) +no ( z .no B ) ) ) ) with typecode |-
72	23 55	naddcomd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no w ) +no ( z .no B ) ) = ( ( z .no B ) +no ( z .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no w ) +no ( z .no B ) ) = ( ( z .no B ) +no ( z .no w ) ) ) with typecode |-
73		oveq1	Could not format ( d = z -> ( d .no ( B +no f ) ) = ( z .no ( B +no f ) ) ) : No typesetting found for |- ( d = z -> ( d .no ( B +no f ) ) = ( z .no ( B +no f ) ) ) with typecode |-
74		oveq1	Could not format ( d = z -> ( d .no f ) = ( z .no f ) ) : No typesetting found for |- ( d = z -> ( d .no f ) = ( z .no f ) ) with typecode |-
75	58 74	oveq12d	Could not format ( d = z -> ( ( d .no B ) +no ( d .no f ) ) = ( ( z .no B ) +no ( z .no f ) ) ) : No typesetting found for |- ( d = z -> ( ( d .no B ) +no ( d .no f ) ) = ( ( z .no B ) +no ( z .no f ) ) ) with typecode |-
76	73 75	eqeq12d	Could not format ( d = z -> ( ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> ( z .no ( B +no f ) ) = ( ( z .no B ) +no ( z .no f ) ) ) ) : No typesetting found for |- ( d = z -> ( ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) <-> ( z .no ( B +no f ) ) = ( ( z .no B ) +no ( z .no f ) ) ) ) with typecode |-
77	37	oveq2d	Could not format ( f = w -> ( z .no ( B +no f ) ) = ( z .no ( B +no w ) ) ) : No typesetting found for |- ( f = w -> ( z .no ( B +no f ) ) = ( z .no ( B +no w ) ) ) with typecode |-
78		oveq2	Could not format ( f = w -> ( z .no f ) = ( z .no w ) ) : No typesetting found for |- ( f = w -> ( z .no f ) = ( z .no w ) ) with typecode |-
79	78	oveq2d	Could not format ( f = w -> ( ( z .no B ) +no ( z .no f ) ) = ( ( z .no B ) +no ( z .no w ) ) ) : No typesetting found for |- ( f = w -> ( ( z .no B ) +no ( z .no f ) ) = ( ( z .no B ) +no ( z .no w ) ) ) with typecode |-
80	77 79	eqeq12d	Could not format ( f = w -> ( ( z .no ( B +no f ) ) = ( ( z .no B ) +no ( z .no f ) ) <-> ( z .no ( B +no w ) ) = ( ( z .no B ) +no ( z .no w ) ) ) ) : No typesetting found for |- ( f = w -> ( ( z .no ( B +no f ) ) = ( ( z .no B ) +no ( z .no f ) ) <-> ( z .no ( B +no w ) ) = ( ( z .no B ) +no ( z .no w ) ) ) ) with typecode |-
81	6	ad2antrr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> A. d e. A A. f e. C ( d .no ( B +no f ) ) = ( ( d .no B ) +no ( d .no f ) ) ) with typecode |-
82	76 80 81 18 21	rspc2dv	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no w ) ) = ( ( z .no B ) +no ( z .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( z .no ( B +no w ) ) = ( ( z .no B ) +no ( z .no w ) ) ) with typecode |-
83	72 82	eqtr4d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no w ) +no ( z .no B ) ) = ( z .no ( B +no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( z .no w ) +no ( z .no B ) ) = ( z .no ( B +no w ) ) ) with typecode |-
84	83	oveq2d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no C ) ) +no ( ( z .no w ) +no ( z .no B ) ) ) = ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no C ) ) +no ( ( z .no w ) +no ( z .no B ) ) ) = ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) with typecode |-
85	71 84	eqtrd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) = ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) = ( ( A .no ( B +no C ) ) +no ( z .no ( B +no w ) ) ) ) with typecode |-
86	52 70 85	3eltr4d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) with typecode |-
87	54 31	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. On ) with typecode |-
88		naddel1	Could not format ( ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. On /\ ( ( A .no ( B +no C ) ) +no ( z .no w ) ) e. On /\ ( z .no B ) e. On ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) <-> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) ) : No typesetting found for |- ( ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. On /\ ( ( A .no ( B +no C ) ) +no ( z .no w ) ) e. On /\ ( z .no B ) e. On ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) <-> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) ) with typecode |-
89	87 29 55 88	syl3anc	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) <-> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) <-> ( ( ( A .no ( B +no w ) ) +no ( z .no C ) ) +no ( z .no B ) ) e. ( ( ( A .no ( B +no C ) ) +no ( z .no w ) ) +no ( z .no B ) ) ) ) with typecode |-
90	86 89	mpbird	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no ( B +no w ) ) +no ( z .no C ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) with typecode |-
91	47 90	eqeltrd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( ( z .no C ) +no ( A .no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) with typecode |-
92	26 29 36 91	ontr2d	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no ( Y +no ( z .no w ) ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) with typecode |-
93	24 92	eqeltrd	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) with typecode |-
94	16 17	naddcld	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no Y ) e. On ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no Y ) e. On ) with typecode |-
95		naddel1	Could not format ( ( ( ( A .no B ) +no Y ) e. On /\ ( A .no ( B +no C ) ) e. On /\ ( z .no w ) e. On ) -> ( ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) <-> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) ) : No typesetting found for |- ( ( ( ( A .no B ) +no Y ) e. On /\ ( A .no ( B +no C ) ) e. On /\ ( z .no w ) e. On ) -> ( ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) <-> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) ) with typecode |-
96	94 28 23 95	syl3anc	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) <-> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) <-> ( ( ( A .no B ) +no Y ) +no ( z .no w ) ) e. ( ( A .no ( B +no C ) ) +no ( z .no w ) ) ) ) with typecode |-
97	93 96	mpbird	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( ( z e. A /\ w e. C ) /\ ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) with typecode |-
98	97	expr	Could not format ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( z e. A /\ w e. C ) ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) ) : No typesetting found for |- ( ( ( ph /\ Y e. ( A .no C ) ) /\ ( z e. A /\ w e. C ) ) -> ( ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) ) with typecode |-
99	98	rexlimdvva	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> ( E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> ( E. z e. A E. w e. C ( Y +no ( z .no w ) ) C_ ( ( z .no C ) +no ( A .no w ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) ) with typecode |-
100	13 99	sylbid	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> ( Y e. ( A .no C ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> ( Y e. ( A .no C ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) ) with typecode |-
101	100	syldbl2	Could not format ( ( ph /\ Y e. ( A .no C ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) : No typesetting found for |- ( ( ph /\ Y e. ( A .no C ) ) -> ( ( A .no B ) +no Y ) e. ( A .no ( B +no C ) ) ) with typecode |-