Theorem bj-equsal1ti

Description: Inference associated with bj-equsal1t . (Contributed by BJ, 30-Sep-2018)

	Ref	Expression
Hypothesis	bj-equsal1ti.1	$$⊢Ⅎx\phi$$
Assertion	bj-equsal1ti	$$⊢\forall x\left(x=y\to \phi \right)\leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		bj-equsal1ti.1	$$⊢Ⅎx\phi$$
2		bj-equsal1t	$$⊢Ⅎx\phi \to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \phi \right)$$
3	1 2	ax-mp	$$⊢\forall x\left(x=y\to \phi \right)\leftrightarrow \phi$$