Theorem addsdilem4

Description: Lemma for addsdi . Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025)

	Ref	Expression
Hypotheses	addsdilem4.1	$$⊢\phi \to A\in \mathrm{No}$$
	addsdilem4.2	$$⊢\phi \to B\in \mathrm{No}$$
	addsdilem4.3	$$⊢\phi \to C\in \mathrm{No}$$
	addsdilem4.4	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) with typecode |-
	addsdilem4.5	No typesetting found for |- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) with typecode |-
	addsdilem4.6	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) with typecode |-
	addsdilem4.7	No typesetting found for |- ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
	addsdilem4.8	No typesetting found for |- ( ps -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) ) with typecode |-
Assertion	addsdilem4	Could not format assertion : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addsdilem4.1	$$⊢\phi \to A\in \mathrm{No}$$
2		addsdilem4.2	$$⊢\phi \to B\in \mathrm{No}$$
3		addsdilem4.3	$$⊢\phi \to C\in \mathrm{No}$$
4		addsdilem4.4	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) with typecode |-
5		addsdilem4.5	Could not format ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) : No typesetting found for |- ( ph -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) with typecode |-
6		addsdilem4.6	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) : No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) with typecode |-
7		addsdilem4.7	Could not format ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ps -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
8		addsdilem4.8	Could not format ( ps -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) ) : No typesetting found for |- ( ps -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) ) with typecode |-
9		oveq1	Could not format ( xO = X -> ( xO x.s ( B +s C ) ) = ( X x.s ( B +s C ) ) ) : No typesetting found for |- ( xO = X -> ( xO x.s ( B +s C ) ) = ( X x.s ( B +s C ) ) ) with typecode |-
10		oveq1	Could not format ( xO = X -> ( xO x.s B ) = ( X x.s B ) ) : No typesetting found for |- ( xO = X -> ( xO x.s B ) = ( X x.s B ) ) with typecode |-
11		oveq1	Could not format ( xO = X -> ( xO x.s C ) = ( X x.s C ) ) : No typesetting found for |- ( xO = X -> ( xO x.s C ) = ( X x.s C ) ) with typecode |-
12	10 11	oveq12d	Could not format ( xO = X -> ( ( xO x.s B ) +s ( xO x.s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s B ) +s ( xO x.s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) with typecode |-
13	9 12	eqeq12d	Could not format ( xO = X -> ( ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) <-> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) <-> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) ) with typecode |-
14	4	adantr	Could not format ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( xO x.s ( B +s C ) ) = ( ( xO x.s B ) +s ( xO x.s C ) ) ) with typecode |-
15	7	adantl	Could not format ( ( ph /\ ps ) -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> X e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
16	13 14 15	rspcdva	Could not format ( ( ph /\ ps ) -> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s ( B +s C ) ) = ( ( X x.s B ) +s ( X x.s C ) ) ) with typecode |-
17		oveq2	Could not format ( zO = Z -> ( B +s zO ) = ( B +s Z ) ) : No typesetting found for |- ( zO = Z -> ( B +s zO ) = ( B +s Z ) ) with typecode |-
18	17	oveq2d	Could not format ( zO = Z -> ( A x.s ( B +s zO ) ) = ( A x.s ( B +s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( A x.s ( B +s zO ) ) = ( A x.s ( B +s Z ) ) ) with typecode |-
19		oveq2	Could not format ( zO = Z -> ( A x.s zO ) = ( A x.s Z ) ) : No typesetting found for |- ( zO = Z -> ( A x.s zO ) = ( A x.s Z ) ) with typecode |-
20	19	oveq2d	Could not format ( zO = Z -> ( ( A x.s B ) +s ( A x.s zO ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( ( A x.s B ) +s ( A x.s zO ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) with typecode |-
21	18 20	eqeq12d	Could not format ( zO = Z -> ( ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) <-> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) ) : No typesetting found for |- ( zO = Z -> ( ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) <-> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) ) with typecode |-
22	5	adantr	Could not format ( ( ph /\ ps ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( A x.s ( B +s zO ) ) = ( ( A x.s B ) +s ( A x.s zO ) ) ) with typecode |-
23	8	adantl	Could not format ( ( ph /\ ps ) -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> Z e. ( ( _Left ` C ) u. ( _Right ` C ) ) ) with typecode |-
24	21 22 23	rspcdva	Could not format ( ( ph /\ ps ) -> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( A x.s ( B +s Z ) ) = ( ( A x.s B ) +s ( A x.s Z ) ) ) with typecode |-
25	16 24	oveq12d	Could not format ( ( ph /\ ps ) -> ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) = ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) = ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) ) with typecode |-
26		oveq1	Could not format ( xO = X -> ( xO x.s ( B +s zO ) ) = ( X x.s ( B +s zO ) ) ) : No typesetting found for |- ( xO = X -> ( xO x.s ( B +s zO ) ) = ( X x.s ( B +s zO ) ) ) with typecode |-
27		oveq1	Could not format ( xO = X -> ( xO x.s zO ) = ( X x.s zO ) ) : No typesetting found for |- ( xO = X -> ( xO x.s zO ) = ( X x.s zO ) ) with typecode |-
28	10 27	oveq12d	Could not format ( xO = X -> ( ( xO x.s B ) +s ( xO x.s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s B ) +s ( xO x.s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) with typecode |-
29	26 28	eqeq12d	Could not format ( xO = X -> ( ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) <-> ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) ) : No typesetting found for |- ( xO = X -> ( ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) <-> ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) ) ) with typecode |-
30	17	oveq2d	Could not format ( zO = Z -> ( X x.s ( B +s zO ) ) = ( X x.s ( B +s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( X x.s ( B +s zO ) ) = ( X x.s ( B +s Z ) ) ) with typecode |-
31		oveq2	Could not format ( zO = Z -> ( X x.s zO ) = ( X x.s Z ) ) : No typesetting found for |- ( zO = Z -> ( X x.s zO ) = ( X x.s Z ) ) with typecode |-
32	31	oveq2d	Could not format ( zO = Z -> ( ( X x.s B ) +s ( X x.s zO ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) : No typesetting found for |- ( zO = Z -> ( ( X x.s B ) +s ( X x.s zO ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) with typecode |-
33	30 32	eqeq12d	Could not format ( zO = Z -> ( ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) <-> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) ) : No typesetting found for |- ( zO = Z -> ( ( X x.s ( B +s zO ) ) = ( ( X x.s B ) +s ( X x.s zO ) ) <-> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) ) with typecode |-
34	6	adantr	Could not format ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) A. zO e. ( ( _Left ` C ) u. ( _Right ` C ) ) ( xO x.s ( B +s zO ) ) = ( ( xO x.s B ) +s ( xO x.s zO ) ) ) with typecode |-
35	29 33 34 15 23	rspc2dv	Could not format ( ( ph /\ ps ) -> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s ( B +s Z ) ) = ( ( X x.s B ) +s ( X x.s Z ) ) ) with typecode |-
36	25 35	oveq12d	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( ( X x.s B ) +s ( X x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( ( X x.s B ) +s ( X x.s Z ) ) ) ) with typecode |-
37		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
38		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
39	37 38	unssi	Could not format ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No : No typesetting found for |- ( ( _Left ` A ) u. ( _Right ` A ) ) C_ No with typecode |-
40	39 7	sselid	$$⊢\psi \to X\in \mathrm{No}$$
41	40	adantl	$$⊢\left(\phi \wedge \psi \right)\to X\in \mathrm{No}$$
42	2	adantr	$$⊢\left(\phi \wedge \psi \right)\to B\in \mathrm{No}$$
43	41 42	mulscld	Could not format ( ( ph /\ ps ) -> ( X x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s B ) e. No ) with typecode |-
44	3	adantr	$$⊢\left(\phi \wedge \psi \right)\to C\in \mathrm{No}$$
45	41 44	mulscld	Could not format ( ( ph /\ ps ) -> ( X x.s C ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s C ) e. No ) with typecode |-
46	43 45	addscld	Could not format ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) e. No ) with typecode |-
47	1 2	mulscld	Could not format ( ph -> ( A x.s B ) e. No ) : No typesetting found for |- ( ph -> ( A x.s B ) e. No ) with typecode |-
48	47	adantr	Could not format ( ( ph /\ ps ) -> ( A x.s B ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( A x.s B ) e. No ) with typecode |-
49	1	adantr	$$⊢\left(\phi \wedge \psi \right)\to A\in \mathrm{No}$$
50		leftssno	Could not format ( _Left ` C ) C_ No : No typesetting found for |- ( _Left ` C ) C_ No with typecode |-
51		rightssno	Could not format ( _Right ` C ) C_ No : No typesetting found for |- ( _Right ` C ) C_ No with typecode |-
52	50 51	unssi	Could not format ( ( _Left ` C ) u. ( _Right ` C ) ) C_ No : No typesetting found for |- ( ( _Left ` C ) u. ( _Right ` C ) ) C_ No with typecode |-
53	52 8	sselid	$$⊢\psi \to Z\in \mathrm{No}$$
54	53	adantl	$$⊢\left(\phi \wedge \psi \right)\to Z\in \mathrm{No}$$
55	49 54	mulscld	Could not format ( ( ph /\ ps ) -> ( A x.s Z ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( A x.s Z ) e. No ) with typecode |-
56	48 55	addscld	Could not format ( ( ph /\ ps ) -> ( ( A x.s B ) +s ( A x.s Z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( A x.s B ) +s ( A x.s Z ) ) e. No ) with typecode |-
57	46 56	addscld	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) e. No ) with typecode |-
58	41 54	mulscld	Could not format ( ( ph /\ ps ) -> ( X x.s Z ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( X x.s Z ) e. No ) with typecode |-
59	57 43 58	subsubs4d	Could not format ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( ( X x.s B ) +s ( X x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( ( X x.s B ) +s ( X x.s Z ) ) ) ) with typecode |-
60	46 56 43	addsubsd	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) = ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) ) with typecode |-
61	43 45	addscomd	Could not format ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) = ( ( X x.s C ) +s ( X x.s B ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s B ) +s ( X x.s C ) ) = ( ( X x.s C ) +s ( X x.s B ) ) ) with typecode |-
62	61	oveq1d	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) = ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) = ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) ) with typecode |-
63		pncans	Could not format ( ( ( X x.s C ) e. No /\ ( X x.s B ) e. No ) -> ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) = ( X x.s C ) ) : No typesetting found for |- ( ( ( X x.s C ) e. No /\ ( X x.s B ) e. No ) -> ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) = ( X x.s C ) ) with typecode |-
64	45 43 63	syl2anc	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) = ( X x.s C ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s C ) +s ( X x.s B ) ) -s ( X x.s B ) ) = ( X x.s C ) ) with typecode |-
65	62 64	eqtrd	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) = ( X x.s C ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) = ( X x.s C ) ) with typecode |-
66	65	oveq1d	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) = ( ( X x.s C ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) -s ( X x.s B ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) = ( ( X x.s C ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) ) with typecode |-
67	45 48 55	adds12d	Could not format ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) = ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) = ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) ) with typecode |-
68	60 66 67	3eqtrd	Could not format ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) = ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) = ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) ) with typecode |-
69	68	oveq1d	Could not format ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) -s ( X x.s Z ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) -s ( X x.s Z ) ) ) with typecode |-
70	45 55	addscld	Could not format ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( A x.s Z ) ) e. No ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( X x.s C ) +s ( A x.s Z ) ) e. No ) with typecode |-
71	48 70 58	addsubsassd	Could not format ( ( ph /\ ps ) -> ( ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) -s ( X x.s Z ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( A x.s B ) +s ( ( X x.s C ) +s ( A x.s Z ) ) ) -s ( X x.s Z ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) ) with typecode |-
72	69 71	eqtrd	Could not format ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( ( ( X x.s B ) +s ( X x.s C ) ) +s ( ( A x.s B ) +s ( A x.s Z ) ) ) -s ( X x.s B ) ) -s ( X x.s Z ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) ) with typecode |-
73	36 59 72	3eqtr2d	Could not format ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) ) : No typesetting found for |- ( ( ph /\ ps ) -> ( ( ( X x.s ( B +s C ) ) +s ( A x.s ( B +s Z ) ) ) -s ( X x.s ( B +s Z ) ) ) = ( ( A x.s B ) +s ( ( ( X x.s C ) +s ( A x.s Z ) ) -s ( X x.s Z ) ) ) ) with typecode |-