Theorem sbbidvOLD

Description: Obsolete version of sbbidv as of 6-Jul-2023. Deduction substituting both sides of a biconditional, with ph and x disjoint. See also sbbid . (Contributed by Wolf Lammen, 6-May-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbbidv.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	sbbidvOLD	$$⊢\phi \to \left(\left[y/x\right]\psi \leftrightarrow \left[y/x\right]\chi \right)$$

Proof

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