Description: Define the property of a wff ph that the setvar variables x and
y are interchangeable. For an alternate definition using implicit
substitution and a temporary setvar variable see ichcircshi .
Another, equivalent definition using two temporary setvar variables is
provided in dfich2 . (Contributed by AV, 29-Jul-2023)