This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer


Syntax definition wich

Description: Extend wff notation to include the property of a wff ph that the setvar variables x and y are interchangeable. Read this notation as " x and y are interchangeable in wff ph ".

Ref Expression
Assertion wich wff x y φ