Thanks a lot Giovanni and Alexander for the answers In one of the proof that I must write, I have the asumption |- ( ph -> ( j = ( k-K ) -> A = B ) ) where ph may be any wff I would love to have $e |- ( ( ph /\ x = Y ) -> A = B ) $ as this would enable me to use fsumshift
Is there a trick to use fsumshift, as is in this situation ? Or is my only hope the deduiction theorem/or proving a version of fsumshift with the hypothesis $e |- ( ( ph /\ x = Y ) -> A = B ) $ ? Alexander, when you say "the patterns $e |- ( x = Y -> A = B ) $. or $e |- ( ( ph /\ x = Y ) -> A = B ) $. for hypotheses are also allowed for deduction style theorems", do you suggest that they are equivalent ? IMO, the first hypothesis is stronger than the second one. -- 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/e2ad36a0-41ae-4c91-99ed-b0d37f3f2deb%40googlegroups.com.
