Metamath Proof Explorer


Theorem elimhyps2

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

Ref Expression
Hypothesis elimhyps2.1 [˙B/x]˙φ
Assertion elimhyps2 [˙if[˙A/x]˙φAB/x]˙φ

Proof

Step Hyp Ref Expression
1 elimhyps2.1 [˙B/x]˙φ
2 dfsbcq A=if[˙A/x]˙φAB[˙A/x]˙φ[˙if[˙A/x]˙φAB/x]˙φ
3 dfsbcq B=if[˙A/x]˙φAB[˙B/x]˙φ[˙if[˙A/x]˙φAB/x]˙φ
4 2 3 1 elimhyp [˙if[˙A/x]˙φAB/x]˙φ