Theorem pm2.61ne is the following: Hypotheses: pm2.61ne.1 |- ( A = B -> ( ps <-> ch ) ) pm2.61ne.2 |- ( ( ph and A =/= B ) -> ps ) pm2.61ne/3 |- ( ph -> ch )
Assertion: pm2.61ne |- ( ph -> ps ) Question 1. Why isn't the first hypothesis given in the weaker condition: pm2.61ne.1weaker |- ( A = B -> ( ch -> ps ) ) Question 2. How does this "new foundations" fit in with metamath? It seems like "new foundations" is being mixed together with "zfc foundation". For example, Theorem msqge0 that asserts A in R -> 0 <= A * A uses pm2.61ne in its proof. -- 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/4765307e-2a18-40aa-a754-7591522e4305n%40googlegroups.com.
