On March 4, 2020 5:58:12 AM PST, 'Stanislas Polu' via Metamath
<[email protected]> wrote:
> the starting point seems to consist in applying
>spesbcd[2], but I'm unclear on how to breach the difference between
>`E. c ph` and `E. c e. A ph` as it does not seem to exist an
>equivalent for the latter?
The direct answer to this question would appear to be
http://us.metamath.org/mpeuni/rspsbc.html
There are usually a lot of ways to arrange this kind of logic though, and often
the theorems using implicit substitution are easier to use, perhaps something
like http://us.metamath.org/mpeuni/rspcev.html
Hope that isn't too bewildering. To get started it is more important to find
one way that works, and worry about all the variations later (or let the
minimizer worry about them).
--
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/7C007903-689F-46B5-A616-779B3660F773%40panix.com.
