Metamath Proof Explorer


Theorem spcimdv

Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 spcimdv.1 φAB
2 spcimdv.2 φx=Aψχ
3 elisset ABxx=A
4 1 3 syl φxx=A
5 2 ex φx=Aψχ
6 5 eximdv φxx=Axψχ
7 4 6 mpd φxψχ
8 19.36v xψχxψχ
9 7 8 sylib φxψχ