Theorem sbcbidvOLD

Description: Obsolete version of sbcbidv as of 1-Dec-2023. (Contributed by NM, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbcbidv.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	sbcbidvOLD	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcbidv.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2		nfv	$$⊢Ⅎx\phi$$
3	2 1	sbcbid	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \right)$$