On Thursday, October 31, 2019 at 1:55:27 PM UTC+1, Norman Megill wrote:
>
> We could add ph to every such hypothesis to make it more general-purpose,
> but 99% of the time it wouldn't be needed and would make all other proofs
> using it (as well as the theorem itself) slightly longer. Not to mention
> that it would be a huge retrofit to do this throughout set.mm. I will
> concede there may be a few cases where it would be advantageous to do
> things other than prove a simple substitution with the hypothesis, but
> overall I believe it is rare and does not justify adding ph everywhere.
>
> I tried to identify all the theorems in set.mm (excluding the mathboxes)
which would be concerned - I found about 70 of them (see attachment
deduct_th_eq_hyp.txt). On the other hand, there are about 50 theorema in
deduction form having the form $e |- ( ( ph /\ x = ... ) -> ... ) $. (see
attachment deduct_th_ph_eq_hyp.txt). So there is no big difference.
Therefore, I still would propose to recommend to use the form $e |- ( ( ph
/\ x = ... ) -> ... ) $. in deduction style. Already existing theorems need
not to be rewritten (by the way, many of them have no "d" at the end..).
>
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/351cfee0-e03b-4d61-b839-694b61641bb0%40googlegroups.com.
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 ) )
$.Theorems written in deduction form, using hypotheses of the kind
$e |- ( x = ... -> ... ) $.
rabxfrd
reuxfrd
fnmptfvd
fliftfun
fliftval
fmpt2co
qliftfun
qliftval
findcard2d
indcardi
ltord1
leord1
eqord1
ltord2
leord2
eqord2
uzindi
fsum
fsumf1o
fsum1p
fsump1
fsump1i
fsum2d
fsumxp
fsumcnv
fsumrev
fsumshft
fsumshftm
fsumrev2
fsum0diag2
fsumge1
fsumtscopo
fsumtscop
fsumparts
isumshft
isumnn0nn
iserodd
pcmpt
issubmd
mrcmndind
gsummptshft
gsummhm2
gsumunsn
mpfind
pf1ind
cnmpt11
cnmptkk
cnmptk1p
cnmptlimc
limcco
dvmptco
dvle
dvfsumle
dvfsumabs
dvfsumrlimf
dvfsumrlim
dvfsumrlim3
dvfsum2
itgsubstlem
rlimcnp
rlimcnp2
rlimcnp3
xrlimcnp
fsumdvdscom
dvdsflsumcom
musumsum
fsumdvdsmul
fsumvma
fsumvma2
dchrelbasd
dchrisum
