Metamath Proof Explorer


Theorem elimhyps

Description: A version of elimhyp using explicit substitution. (Contributed by NM, 15-Jun-2019)

Ref Expression
Hypothesis elimhyps.1 [˙B/x]˙φ
Assertion elimhyps [˙ifφxB/x]˙φ

Proof

Step Hyp Ref Expression
1 elimhyps.1 [˙B/x]˙φ
2 sbceq1a x=ifφxBφ[˙ifφxB/x]˙φ
3 dfsbcq B=ifφxB[˙B/x]˙φ[˙ifφxB/x]˙φ
4 2 3 1 elimhyp [˙ifφxB/x]˙φ