Theorem dedths2

Description: Generalization of dedths that is not useful unless we can separately prove |- A e. _V . (Contributed by NM, 13-Jun-2019)

	Ref	Expression
Hypothesis	dedths2.1	|- [. if ( [. A / x ]. ph , A , B ) / x ]. ps
Assertion	dedths2	|- ( [. A / x ]. ph -> [. A / x ]. ps )

Proof

Step	Hyp	Ref	Expression
1		dedths2.1	|- [. if ( [. A / x ]. ph , A , B ) / x ]. ps
2		dfsbcq	|- ( A = if ( [. A / x ]. ph , A , B ) -> ( [. A / x ]. ps <-> [. if ( [. A / x ]. ph , A , B ) / x ]. ps ) )
3	2 1	dedth	|- ( [. A / x ]. ph -> [. A / x ]. ps )