Metamath Proof Explorer


Theorem rspccv

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006)

Ref Expression
Hypothesis rspcv.1 x = A φ ψ
Assertion rspccv x B φ A B ψ

Proof

Step Hyp Ref Expression
1 rspcv.1 x = A φ ψ
2 1 rspcv A B x B φ ψ
3 2 com12 x B φ A B ψ