Metamath Proof Explorer

Theorem subsym1

Description: A symmetry with [ x / y ] .

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

		Ref	Expression
	Assertion	subsym1	$⊢ [y/ x] [y/ x] ⊥ \to [y/ x] φ$

Step	Hyp	Ref	Expression
1		sbv	$⊢ [y/ x] ⊥ \leftrightarrow ⊥$
2		falim	$⊢ ⊥ \to φ$
3	1 2	sylbi	$⊢ [y/ x] ⊥ \to φ$
4	3	sbimi	$⊢ [y/ x] [y/ x] ⊥ \to [y/ x] φ$