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	⊢ ( ∀ 𝑥 ∀ 𝑥 ⊥ → ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		falim	⊢ ( ⊥ → ∀ 𝑥 𝜑 )
2	1	sps	⊢ ( ∀ 𝑥 ⊥ → ∀ 𝑥 𝜑 )
3	2	sps	⊢ ( ∀ 𝑥 ∀ 𝑥 ⊥ → ∀ 𝑥 𝜑 )