Theorem nadddilem3

Description: Lemma for nadddi . Prove a subcase of the forward implication. (Contributed by Scott Fenton, 3-Aug-2026)

	Ref	Expression
Hypotheses	nadddilem3.1	$$⊢\phi \to A\in \mathrm{On}$$
	nadddilem3.2	$$⊢\phi \to B\in \mathrm{On}$$
	nadddilem3.3	$$⊢\phi \to C\in \mathrm{On}$$
	nadddilem3.4	$$⊢\phi \to X\in A$$
	nadddilem3.5	$$⊢\phi \to Y\in \left(B+C\right)$$
	nadddilem3.6	$$⊢\phi \to Z\in B$$
	nadddilem3.7	$$⊢\phi \to Y\subseteq Z+C$$
	nadddilem3.8	No typesetting found for |- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
	nadddilem3.9	No typesetting found for |- ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) ) with typecode |-
	nadddilem3.10	No typesetting found for |- ( ph -> A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) ) with typecode |-
Assertion	nadddilem3	Could not format assertion : No typesetting found for |- ( ph -> ( ( X .no ( B +no C ) ) +no ( A .no Y ) ) e. ( ( ( A .no B ) +no ( A .no C ) ) +no ( X .no Y ) ) ) with typecode |-

Proof

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