Theorem spsbbi

Description: Biconditional property for substitution. Closed form of sbbii . Specialization of biconditional. (Contributed by NM, 2-Jun-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020)

	Ref	Expression
Assertion	spsbbi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\left[t/x\right]\phi \leftrightarrow \left[t/x\right]\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		biimp	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\phi \to \psi \right)$$
2	1	alimi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \forall x\left(\phi \to \psi \right)$$
3		spsbim	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\left[t/x\right]\phi \to \left[t/x\right]\psi \right)$$
4	2 3	syl	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\left[t/x\right]\phi \to \left[t/x\right]\psi \right)$$
5		biimpr	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\psi \to \phi \right)$$
6	5	alimi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \forall x\left(\psi \to \phi \right)$$
7		spsbim	$$⊢\forall x\left(\psi \to \phi \right)\to \left(\left[t/x\right]\psi \to \left[t/x\right]\phi \right)$$
8	6 7	syl	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\left[t/x\right]\psi \to \left[t/x\right]\phi \right)$$
9	4 8	impbid	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\left[t/x\right]\phi \leftrightarrow \left[t/x\right]\psi \right)$$