Theorems written in deduction form, using hypotheses of the kind 
$e |- ( ( ph /\ x = ... ) -> ... ) $.

	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 ) $.