Re: [Metamath] How to do substitutions in Metamath?

[Giovanni Mascellani]

Hi,

Il 02/06/19 12:44, Tony ha scritto:
> I don't see any suitable theorems to use.  Like for instance:
> 
> [𝑥 / 𝑦] (𝜑 ↔  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ↔ [𝑥 / 𝑦]𝜓 ),
> [𝑥 / 𝑦] (𝜑 ∧  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ∧ [𝑥 / 𝑦]𝜓 ).

Look for sbcan and those that immediately follow:

  http://us.metamath.org/mpeuni/mmtheorems33.html#sbcan

HTH, Giovanni.
-- 
Giovanni Mascellani <g.mascell...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

-- 
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2e1ba7f1-5c71-16ad-a5da-960b4743c956%40gmail.com.

signature.asc
Description: OpenPGP digital signature