Theorem nadddilem2

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

	Ref	Expression
Hypotheses	nadddilem2.1	$$⊢\phi \to A\in \mathrm{On}$$
	nadddilem2.2	$$⊢\phi \to B\in \mathrm{On}$$
	nadddilem2.3	$$⊢\phi \to C\in \mathrm{On}$$
	nadddilem2.4	No typesetting found for |- ( ph -> A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) ) with typecode |-
	nadddilem2.5	No typesetting found for |- ( ph -> A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) ) with typecode |-
	nadddilem2.6	No typesetting found for |- ( ph -> A. f e. C ( A .no ( B +no f ) ) = ( ( A .no B ) +no ( A .no f ) ) ) with typecode |-
	nadddilem2.7	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 |-
	nadddilem2.8	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	nadddilem2	Could not format assertion : No typesetting found for |- ( ph -> ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nadddilem2.1	$$⊢\phi \to A\in \mathrm{On}$$
2		nadddilem2.2	$$⊢\phi \to B\in \mathrm{On}$$
3		nadddilem2.3	$$⊢\phi \to C\in \mathrm{On}$$
4		nadddilem2.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		nadddilem2.5	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 |-
6		nadddilem2.6	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 |-
7		nadddilem2.7	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 |-
8		nadddilem2.8	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 |-
9		oveq1	Could not format ( d = p -> ( d .no ( B +no C ) ) = ( p .no ( B +no C ) ) ) : No typesetting found for |- ( d = p -> ( d .no ( B +no C ) ) = ( p .no ( B +no C ) ) ) with typecode |-
10		oveq1	Could not format ( d = p -> ( d .no B ) = ( p .no B ) ) : No typesetting found for |- ( d = p -> ( d .no B ) = ( p .no B ) ) with typecode |-
11		oveq1	Could not format ( d = p -> ( d .no C ) = ( p .no C ) ) : No typesetting found for |- ( d = p -> ( d .no C ) = ( p .no C ) ) with typecode |-
12	10 11	oveq12d	Could not format ( d = p -> ( ( d .no B ) +no ( d .no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no B ) +no ( d .no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) with typecode |-
13	9 12	eqeq12d	Could not format ( d = p -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) ) with typecode |-
14	13	cbvralvw	Could not format ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) : No typesetting found for |- ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) ) with typecode |-
15	2 3	naddcomd	$$⊢\phi \to B+C=C+B$$
16	15	oveq2d	Could not format ( ph -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) ) : No typesetting found for |- ( ph -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) ) with typecode |-
17	16	adantr	Could not format ( ( ph /\ p e. A ) -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( p .no ( B +no C ) ) = ( p .no ( C +no B ) ) ) with typecode |-
18	1	adantr	$$⊢\left(\phi \wedge p\in A\right)\to A\in \mathrm{On}$$
19		simpr	$$⊢\left(\phi \wedge p\in A\right)\to p\in A$$
20	18 19	onelond	$$⊢\left(\phi \wedge p\in A\right)\to p\in \mathrm{On}$$
21	2	adantr	$$⊢\left(\phi \wedge p\in A\right)\to B\in \mathrm{On}$$
22	20 21	nmulcld	Could not format ( ( ph /\ p e. A ) -> ( p .no B ) e. On ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( p .no B ) e. On ) with typecode |-
23	3	adantr	$$⊢\left(\phi \wedge p\in A\right)\to C\in \mathrm{On}$$
24	20 23	nmulcld	Could not format ( ( ph /\ p e. A ) -> ( p .no C ) e. On ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( p .no C ) e. On ) with typecode |-
25	22 24	naddcomd	Could not format ( ( ph /\ p e. A ) -> ( ( p .no B ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no B ) ) ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( ( p .no B ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no B ) ) ) with typecode |-
26	17 25	eqeq12d	Could not format ( ( ph /\ p e. A ) -> ( ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ( ph /\ p e. A ) -> ( ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) with typecode |-
27	26	ralbidva	Could not format ( ph -> ( A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. p e. A ( p .no ( B +no C ) ) = ( ( p .no B ) +no ( p .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) with typecode |-
28	14 27	bitrid	Could not format ( ph -> ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) : No typesetting found for |- ( ph -> ( A. d e. A ( d .no ( B +no C ) ) = ( ( d .no B ) +no ( d .no C ) ) <-> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) ) with typecode |-
29	4 28	mpbid	Could not format ( ph -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) : No typesetting found for |- ( ph -> A. p e. A ( p .no ( C +no B ) ) = ( ( p .no C ) +no ( p .no B ) ) ) with typecode |-
30		oveq1	$$⊢e=q\to e+C=q+C$$
31	30	oveq2d	Could not format ( e = q -> ( A .no ( e +no C ) ) = ( A .no ( q +no C ) ) ) : No typesetting found for |- ( e = q -> ( A .no ( e +no C ) ) = ( A .no ( q +no C ) ) ) with typecode |-
32		oveq2	Could not format ( e = q -> ( A .no e ) = ( A .no q ) ) : No typesetting found for |- ( e = q -> ( A .no e ) = ( A .no q ) ) with typecode |-
33	32	oveq1d	Could not format ( e = q -> ( ( A .no e ) +no ( A .no C ) ) = ( ( A .no q ) +no ( A .no C ) ) ) : No typesetting found for |- ( e = q -> ( ( A .no e ) +no ( A .no C ) ) = ( ( A .no q ) +no ( A .no C ) ) ) with typecode |-
34	31 33	eqeq12d	Could not format ( e = q -> ( ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) ) ) : No typesetting found for |- ( e = q -> ( ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) ) ) with typecode |-
35	34	cbvralvw	Could not format ( A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) ) : No typesetting found for |- ( A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) ) with typecode |-
36	2	adantr	$$⊢\left(\phi \wedge q\in B\right)\to B\in \mathrm{On}$$
37		simpr	$$⊢\left(\phi \wedge q\in B\right)\to q\in B$$
38	36 37	onelond	$$⊢\left(\phi \wedge q\in B\right)\to q\in \mathrm{On}$$
39	3	adantr	$$⊢\left(\phi \wedge q\in B\right)\to C\in \mathrm{On}$$
40	38 39	naddcomd	$$⊢\left(\phi \wedge q\in B\right)\to q+C=C+q$$
41	40	oveq2d	Could not format ( ( ph /\ q e. B ) -> ( A .no ( q +no C ) ) = ( A .no ( C +no q ) ) ) : No typesetting found for |- ( ( ph /\ q e. B ) -> ( A .no ( q +no C ) ) = ( A .no ( C +no q ) ) ) with typecode |-
42	1	adantr	$$⊢\left(\phi \wedge q\in B\right)\to A\in \mathrm{On}$$
43	42 38	nmulcld	Could not format ( ( ph /\ q e. B ) -> ( A .no q ) e. On ) : No typesetting found for |- ( ( ph /\ q e. B ) -> ( A .no q ) e. On ) with typecode |-
44	42 39	nmulcld	Could not format ( ( ph /\ q e. B ) -> ( A .no C ) e. On ) : No typesetting found for |- ( ( ph /\ q e. B ) -> ( A .no C ) e. On ) with typecode |-
45	43 44	naddcomd	Could not format ( ( ph /\ q e. B ) -> ( ( A .no q ) +no ( A .no C ) ) = ( ( A .no C ) +no ( A .no q ) ) ) : No typesetting found for |- ( ( ph /\ q e. B ) -> ( ( A .no q ) +no ( A .no C ) ) = ( ( A .no C ) +no ( A .no q ) ) ) with typecode |-
46	41 45	eqeq12d	Could not format ( ( ph /\ q e. B ) -> ( ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) <-> ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) ) : No typesetting found for |- ( ( ph /\ q e. B ) -> ( ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) <-> ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) ) with typecode |-
47	46	ralbidva	Could not format ( ph -> ( A. q e. B ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) ) : No typesetting found for |- ( ph -> ( A. q e. B ( A .no ( q +no C ) ) = ( ( A .no q ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) ) with typecode |-
48	35 47	bitrid	Could not format ( ph -> ( A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) ) : No typesetting found for |- ( ph -> ( A. e e. B ( A .no ( e +no C ) ) = ( ( A .no e ) +no ( A .no C ) ) <-> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) ) with typecode |-
49	5 48	mpbid	Could not format ( ph -> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) : No typesetting found for |- ( ph -> A. q e. B ( A .no ( C +no q ) ) = ( ( A .no C ) +no ( A .no q ) ) ) with typecode |-
50		oveq1	Could not format ( d = p -> ( d .no ( e +no C ) ) = ( p .no ( e +no C ) ) ) : No typesetting found for |- ( d = p -> ( d .no ( e +no C ) ) = ( p .no ( e +no C ) ) ) with typecode |-
51		oveq1	Could not format ( d = p -> ( d .no e ) = ( p .no e ) ) : No typesetting found for |- ( d = p -> ( d .no e ) = ( p .no e ) ) with typecode |-
52	51 11	oveq12d	Could not format ( d = p -> ( ( d .no e ) +no ( d .no C ) ) = ( ( p .no e ) +no ( p .no C ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no e ) +no ( d .no C ) ) = ( ( p .no e ) +no ( p .no C ) ) ) with typecode |-
53	50 52	eqeq12d	Could not format ( d = p -> ( ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> ( p .no ( e +no C ) ) = ( ( p .no e ) +no ( p .no C ) ) ) ) : No typesetting found for |- ( d = p -> ( ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> ( p .no ( e +no C ) ) = ( ( p .no e ) +no ( p .no C ) ) ) ) with typecode |-
54	30	oveq2d	Could not format ( e = q -> ( p .no ( e +no C ) ) = ( p .no ( q +no C ) ) ) : No typesetting found for |- ( e = q -> ( p .no ( e +no C ) ) = ( p .no ( q +no C ) ) ) with typecode |-
55		oveq2	Could not format ( e = q -> ( p .no e ) = ( p .no q ) ) : No typesetting found for |- ( e = q -> ( p .no e ) = ( p .no q ) ) with typecode |-
56	55	oveq1d	Could not format ( e = q -> ( ( p .no e ) +no ( p .no C ) ) = ( ( p .no q ) +no ( p .no C ) ) ) : No typesetting found for |- ( e = q -> ( ( p .no e ) +no ( p .no C ) ) = ( ( p .no q ) +no ( p .no C ) ) ) with typecode |-
57	54 56	eqeq12d	Could not format ( e = q -> ( ( p .no ( e +no C ) ) = ( ( p .no e ) +no ( p .no C ) ) <-> ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) ) ) : No typesetting found for |- ( e = q -> ( ( p .no ( e +no C ) ) = ( ( p .no e ) +no ( p .no C ) ) <-> ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) ) ) with typecode |-
58	53 57	cbvral2vw	Could not format ( A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> A. p e. A A. q e. B ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) ) : No typesetting found for |- ( A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> A. p e. A A. q e. B ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) ) with typecode |-
59	40	adantrl	$$⊢\left(\phi \wedge \left(p\in A\wedge q\in B\right)\right)\to q+C=C+q$$
60	59	oveq2d	Could not format ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no ( q +no C ) ) = ( p .no ( C +no q ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no ( q +no C ) ) = ( p .no ( C +no q ) ) ) with typecode |-
61	20	adantrr	$$⊢\left(\phi \wedge \left(p\in A\wedge q\in B\right)\right)\to p\in \mathrm{On}$$
62	38	adantrl	$$⊢\left(\phi \wedge \left(p\in A\wedge q\in B\right)\right)\to q\in \mathrm{On}$$
63	61 62	nmulcld	Could not format ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no q ) e. On ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no q ) e. On ) with typecode |-
64	3	adantr	$$⊢\left(\phi \wedge \left(p\in A\wedge q\in B\right)\right)\to C\in \mathrm{On}$$
65	61 64	nmulcld	Could not format ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no C ) e. On ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( p .no C ) e. On ) with typecode |-
66	63 65	naddcomd	Could not format ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( ( p .no q ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no q ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( ( p .no q ) +no ( p .no C ) ) = ( ( p .no C ) +no ( p .no q ) ) ) with typecode |-
67	60 66	eqeq12d	Could not format ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) <-> ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) ) : No typesetting found for |- ( ( ph /\ ( p e. A /\ q e. B ) ) -> ( ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) <-> ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) ) with typecode |-
68	67	2ralbidva	Could not format ( ph -> ( A. p e. A A. q e. B ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) <-> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) ) : No typesetting found for |- ( ph -> ( A. p e. A A. q e. B ( p .no ( q +no C ) ) = ( ( p .no q ) +no ( p .no C ) ) <-> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) ) with typecode |-
69	58 68	bitrid	Could not format ( ph -> ( A. d e. A A. e e. B ( d .no ( e +no C ) ) = ( ( d .no e ) +no ( d .no C ) ) <-> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) ) : 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 ) ) <-> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) ) with typecode |-
70	7 69	mpbid	Could not format ( ph -> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) : No typesetting found for |- ( ph -> A. p e. A A. q e. B ( p .no ( C +no q ) ) = ( ( p .no C ) +no ( p .no q ) ) ) with typecode |-
71	1 3 2 29 49 70	nadddilem1	Could not format ( ( ph /\ x e. ( A .no B ) ) -> ( ( A .no C ) +no x ) e. ( A .no ( C +no B ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> ( ( A .no C ) +no x ) e. ( A .no ( C +no B ) ) ) with typecode |-
72	1 2	nmulcld	Could not format ( ph -> ( A .no B ) e. On ) : No typesetting found for |- ( ph -> ( A .no B ) e. On ) with typecode |-
73	72	adantr	Could not format ( ( ph /\ x e. ( A .no B ) ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> ( A .no B ) e. On ) with typecode |-
74		simpr	Could not format ( ( ph /\ x e. ( A .no B ) ) -> x e. ( A .no B ) ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> x e. ( A .no B ) ) with typecode |-
75	73 74	onelond	Could not format ( ( ph /\ x e. ( A .no B ) ) -> x e. On ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> x e. On ) with typecode |-
76	1 3	nmulcld	Could not format ( ph -> ( A .no C ) e. On ) : No typesetting found for |- ( ph -> ( A .no C ) e. On ) with typecode |-
77	76	adantr	Could not format ( ( ph /\ x e. ( A .no B ) ) -> ( A .no C ) e. On ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> ( A .no C ) e. On ) with typecode |-
78	75 77	naddcomd	Could not format ( ( ph /\ x e. ( A .no B ) ) -> ( x +no ( A .no C ) ) = ( ( A .no C ) +no x ) ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> ( x +no ( A .no C ) ) = ( ( A .no C ) +no x ) ) with typecode |-
79	15	oveq2d	Could not format ( ph -> ( A .no ( B +no C ) ) = ( A .no ( C +no B ) ) ) : No typesetting found for |- ( ph -> ( A .no ( B +no C ) ) = ( A .no ( C +no B ) ) ) with typecode |-
80	79	adantr	Could not format ( ( ph /\ x e. ( A .no B ) ) -> ( A .no ( B +no C ) ) = ( A .no ( C +no B ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> ( A .no ( B +no C ) ) = ( A .no ( C +no B ) ) ) with typecode |-
81	71 78 80	3eltr4d	Could not format ( ( ph /\ x e. ( A .no B ) ) -> ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( A .no B ) ) -> ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) ) with typecode |-
82	81	ralrimiva	Could not format ( ph -> A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) ) : No typesetting found for |- ( ph -> A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) ) with typecode |-
83	1 2 3 4 6 8	nadddilem1	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 |-
84	83	ralrimiva	Could not format ( ph -> A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) : No typesetting found for |- ( ph -> A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) with typecode |-
85	2 3	naddcld	$$⊢\phi \to B+C\in \mathrm{On}$$
86	1 85	nmulcld	Could not format ( ph -> ( A .no ( B +no C ) ) e. On ) : No typesetting found for |- ( ph -> ( A .no ( B +no C ) ) e. On ) with typecode |-
87		naddle	Could not format ( ( ( A .no B ) e. On /\ ( A .no C ) e. On /\ ( A .no ( B +no C ) ) e. On ) -> ( ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) <-> ( A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) /\ A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) ) ) : No typesetting found for |- ( ( ( A .no B ) e. On /\ ( A .no C ) e. On /\ ( A .no ( B +no C ) ) e. On ) -> ( ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) <-> ( A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) /\ A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) ) ) with typecode |-
88	72 76 86 87	syl3anc	Could not format ( ph -> ( ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) <-> ( A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) /\ A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) <-> ( A. x e. ( A .no B ) ( x +no ( A .no C ) ) e. ( A .no ( B +no C ) ) /\ A. y e. ( A .no C ) ( ( A .no B ) +no y ) e. ( A .no ( B +no C ) ) ) ) ) with typecode |-
89	82 84 88	mpbir2and	Could not format ( ph -> ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) ) : No typesetting found for |- ( ph -> ( ( A .no B ) +no ( A .no C ) ) C_ ( A .no ( B +no C ) ) ) with typecode |-