Theorem csbeq12dv

Description: Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023)

	Ref	Expression
Hypotheses	csbeq12dv.1	$$⊢\phi \to A=C$$
	csbeq12dv.2	$$⊢\phi \to B=D$$
Assertion	csbeq12dv	$$⊢\phi \to ⦋A/x⦌B=⦋C/x⦌D$$

Proof

Step	Hyp	Ref	Expression
1		csbeq12dv.1	$$⊢\phi \to A=C$$
2		csbeq12dv.2	$$⊢\phi \to B=D$$
3	1	csbeq1d	$$⊢\phi \to ⦋A/x⦌B=⦋C/x⦌B$$
4	2	csbeq2dv	$$⊢\phi \to ⦋C/x⦌B=⦋C/x⦌D$$
5	3 4	eqtrd	$$⊢\phi \to ⦋A/x⦌B=⦋C/x⦌D$$