Metamath Proof Explorer


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]˙φAB/x]˙ψ
Assertion dedths2 [˙A/x]˙φ[˙A/x]˙ψ

Proof

Step Hyp Ref Expression
1 dedths2.1 [˙if[˙A/x]˙φAB/x]˙ψ
2 dfsbcq A=if[˙A/x]˙φAB[˙A/x]˙ψ[˙if[˙A/x]˙φAB/x]˙ψ
3 2 1 dedth [˙A/x]˙φ[˙A/x]˙ψ