Theorem unisym1

Description: A symmetry with A. .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011) (Proof shortened by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Assertion	unisym1	$$⊢\forall x\forall x\perp \to \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		falim	$$⊢\perp \to \forall x\phi$$
2	1	sps	$$⊢\forall x\perp \to \forall x\phi$$
3	2	sps	$$⊢\forall x\forall x\perp \to \forall x\phi$$