Hi David, I think the theorem should be zeroimpxpxeqzero $p |- ( x = 0 -> ( x + x ) = 0 ) (with brackets). then you can use eqtrd and oveq12d to replace x by 0, resulting in ( x = 0 -> ( 0 + 0 ) = 0 ). Then apply a1i and 00id.
Alexander On Saturday, May 2, 2020 at 9:55:54 AM UTC+2, David Starner wrote: > > I'm have trouble with this, and I can't find an example in the set.mm. > How would you prove something like zeroimpxpxeqzero $p |- ( x = 0 -> x > + x = 0 ) ? (or x = 1 -> x + x = 2, etc.) I've got a similar problem > in group theory that would be trivial if I could find something to > move the equality across the implication and convert it into 0 + 0 = > 0. > > -- > The standard is written in English . If you have trouble understanding > a particular section, read it again and again and again . . . Sit up > straight. Eat your vegetables. Do not mumble. -- _Pascal_, ISO 7185 > (1991) > -- 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/30b5cc20-97d7-4bee-bba4-1be33de7e2d4%40googlegroups.com.
