Theorem csbeq12dv

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

	Ref	Expression
Hypotheses	csbeq12dv.1	|- ( ph -> A = C )
	csbeq12dv.2	|- ( ph -> B = D )
Assertion	csbeq12dv	|- ( ph -> [_ A / x ]_ B = [_ C / x ]_ D )

Proof

Step	Hyp	Ref	Expression
1		csbeq12dv.1	|- ( ph -> A = C )
2		csbeq12dv.2	|- ( ph -> B = D )
3	1	csbeq1d	|- ( ph -> [_ A / x ]_ B = [_ C / x ]_ B )
4	2	csbeq2dv	|- ( ph -> [_ C / x ]_ B = [_ C / x ]_ D )
5	3 4	eqtrd	|- ( ph -> [_ A / x ]_ B = [_ C / x ]_ D )