Theorem sbbii

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993)

	Ref	Expression
Hypothesis	sbbii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	sbbii	$$⊢\left[t/x\right]\phi \leftrightarrow \left[t/x\right]\psi$$

Proof

Step	Hyp	Ref	Expression
1		sbbii.1	$$⊢\phi \leftrightarrow \psi$$
2	1	biimpi	$$⊢\phi \to \psi$$
3	2	sbimi	$$⊢\left[t/x\right]\phi \to \left[t/x\right]\psi$$
4	1	biimpri	$$⊢\psi \to \phi$$
5	4	sbimi	$$⊢\left[t/x\right]\psi \to \left[t/x\right]\phi$$
6	3 5	impbii	$$⊢\left[t/x\right]\phi \leftrightarrow \left[t/x\right]\psi$$