Why doesn't fsumshft.5 have a ph -> part like other hypotheses ? fsumshft.5 [image: |-] [image: (][image: j] [image: =] [image: (][image: k] [image: -] [image: K][image: )] [image: ->] [image: A] [image: =] [image: B][image: )] Is the same theorem with ( ph -> ( j = ( k-K ) -> A = B ) ) false ? or stupid ? or unnecessary ?
It looks stronger to me as I probably cannot prove it easily from fsumshtf I am still grasping at all the subtleties of Metamath, so I may not understand something important here. Could someone please enlighten me ? Best regards, Olivier -- 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/9fe25b05-3d66-484f-9c1f-801c41a7dff0%40googlegroups.com.
