Metamath Proof Explorer

Theorem spcdv

Description: Rule of specialization, using implicit substitution. Analogous to rspcdv . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses spcimdv.1 φ A B
spcdv.2 φ x = A ψ χ
Assertion spcdv φ x ψ χ


Step Hyp Ref Expression
1 spcimdv.1 φ A B
2 spcdv.2 φ x = A ψ χ
3 2 biimpd φ x = A ψ χ
4 1 3 spcimdv φ x ψ χ