Theorem sbbidOLD

Description: Obsolete version of sbbid as of 10-Jul-2023. Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993) Remove dependency on ax-10 and ax-13 . (Revised by Wolf Lammen, 24-Nov-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sbbidOLD.1	$$⊢Ⅎx\phi$$
	sbbidOLD.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	sbbidOLD	$$⊢\phi \to \left(\left[y/x\right]\psi \leftrightarrow \left[y/x\right]\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbbidOLD.1	$$⊢Ⅎx\phi$$
2		sbbidOLD.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
3	2	biimpd	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	1 3	sbimd	$$⊢\phi \to \left(\left[y/x\right]\psi \to \left[y/x\right]\chi \right)$$
5	2	biimprd	$$⊢\phi \to \left(\chi \to \psi \right)$$
6	1 5	sbimd	$$⊢\phi \to \left(\left[y/x\right]\chi \to \left[y/x\right]\psi \right)$$
7	4 6	impbid	$$⊢\phi \to \left(\left[y/x\right]\psi \leftrightarrow \left[y/x\right]\chi \right)$$