Theorem subsym1

Description: A symmetry with [ x / y ] .

See negsym1 for more information. (Contributed by Anthony Hart, 11-Sep-2011)

	Ref	Expression
Assertion	subsym1	$$⊢\left[y/x\right]\left[y/x\right]\perp \to \left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbv	$$⊢\left[y/x\right]\perp \leftrightarrow \perp$$
2		falim	$$⊢\perp \to \phi$$
3	1 2	sylbi	$$⊢\left[y/x\right]\perp \to \phi$$
4	3	sbimi	$$⊢\left[y/x\right]\left[y/x\right]\perp \to \left[y/x\right]\phi$$