Line 51536:     ralxfrd.3 $e |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) $.
	Line 51558:     ralxfr2d.3 $e |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) $.
	Line 59804:     iota2df.3 $e |- ( ( ph /\ x = B ) -> ( ps <-> ch ) ) $.
	Line 63151:     fvmptd.2 $e |- ( ( ph /\ x = A ) -> B = C ) $.
	Line 63231:     fvmptdf.2 $e |- ( ( ph /\ x = A ) -> B e. V ) $.
	Line 63232:     fvmptdf.3 $e |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) ) $.
	Line 63257:     fvmptdv2.2 $e |- ( ( ph /\ x = A ) -> B e. V ) $.
	Line 63258:     fvmptdv2.3 $e |- ( ( ph /\ x = A ) -> B = C ) $.
	Line 64651:     fmptapd.2 $e |- ( ( ph /\ x = A ) -> C = B ) $.
	Line 64668:     fmptpr.5 $e |- ( ( ph /\ x = A ) -> E = C ) $.
	Line 64669:     fmptpr.6 $e |- ( ( ph /\ x = B ) -> E = D ) $.
	Line 66839:     riota2df.5 $e |- ( ( ph /\ x = B ) -> ( ps <-> ch ) ) $.
	Line 68467:     ovmpt2dx.3 $e |- ( ( ph /\ x = A ) -> D = L ) $.
	Line 68548:     ovmpt2df.2 $e |- ( ( ph /\ x = A ) -> B e. D ) $.
	Line 68581:     ovmpt2dv2.2 $e |- ( ( ph /\ x = A ) -> B e. D ) $.
	Line 75327:     sprmpt2d.2 $e |- ( ( ph /\ v = V /\ e = E ) -> ( ch <-> ps ) ) $.
	Line 77808:     oe0lem.1 $e |- ( ( ph /\ A = (/) ) -> ps ) $.
	Line 216690:     gsumsnd.s $e |- ( ( ph /\ k = M ) -> A = C ) $.
	Line 216714:     gsumzunsnd.s $e |- ( ( ph /\ k = M ) -> X = Y ) $.
	Line 216743:     gsumunsnd.s $e |- ( ( ph /\ k = M ) -> X = Y ) $.
	Line 222411:     gsummgp0.e $e |- ( ( ph /\ n = i ) -> A = B ) $.
	Line 315067:     itgparts.e $e |- ( ( ph /\ x = X ) -> ( A x. C ) = E ) $.
	Line 315068:     itgparts.f $e |- ( ( ph /\ x = Y ) -> ( A x. C ) = F ) $.
	Line 406675:     reuxfr4d.3 $e |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) $.
	Line 406745:     rmoxfrd.3 $e |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) $.
	Line 407268:     iunrdx.2 $e |- ( ( ph /\ y = ( F ` x ) ) -> D = B ) $.
	Line 407613:     disjrdx.2 $e |- ( ( ph /\ y = ( F ` x ) ) -> D = B ) $.
	Line 413026:     gsumsn2.s $e |- ( ( ph /\ k = M ) -> A = C ) $.
	Line 418346:     esumsn.1 $e |- ( ( ph /\ k = M ) -> A = B ) $.
	Line 418379:     esumpr.1 $e |- ( ( ph /\ k = A ) -> C = D ) $.
	Line 418380:     esumpr.2 $e |- ( ( ph /\ k = B ) -> C = E ) $.
	Line 426982:     sgn3da.4 $e |- ( ( ph /\ A = 0 ) -> ch ) $.
	Line 427160:     gsumnunsn.c $e |- ( ( ph /\ k = ( P + 1 ) ) -> B = C ) $.
	Line 439722:     fprodeq0.4 $e |- ( ( ph /\ k = N ) -> A = 0 ) $.
	Line 482922:     sumsnd.3 $e |- ( ( ph /\ k = M ) -> A = B ) $.
	Line 483179:     sumupair.8 $e |- ( ( ph /\ k = A ) -> C = D ) $.
	Line 483180:     sumupair.9 $e |- ( ( ph /\ k = B ) -> C = E ) $.
	Line 504773:     fmptsnd.1 $e |- ( ( ph /\ x = A ) -> B = C ) $.
	Line 504903:     ovmpt2rdx.3 $e |- ( ( ph /\ y = B ) -> C = L ) $.
	Line 505528:     gsumdifsnd.s $e |- ( ( ph /\ k = M ) -> X = Y ) $.
	Line 505548:     gsumsndf.s $e |- ( ( ph /\ k = M ) -> A = C ) $.
	Line 505593:     gsumdifsndf.s $e |- ( ( ph /\ k = M ) -> X = Y ) $.
	Line 533009:     bj-cbvaldvav.1 $e |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) $.
	Line 536883:     riotasv2d.5 $e |- ( ( ph /\ y = E ) -> ( ps <-> ch ) ) $.
	Line 536884:     riotasv2d.6 $e |- ( ( ph /\ y = E ) -> C = F ) $.
	Line 536939:     riotasv3d.4 $e |- ( ( ph /\ C = D ) -> ( ch <-> th ) ) $.