Metamath Proof Explorer

Theorem chvarfv

Description: Implicit substitution of y for x into a theorem. Version of chvar with a disjoint variable condition, which does not require ax-13 . (Contributed by Raph Levien, 9-Jul-2003) (Revised by BJ, 31-May-2019)

Ref Expression
Hypotheses x ψ
chvarfv.1 x = y φ ψ
chvarfv.2 φ
Assertion chvarfv ψ


Step Hyp Ref Expression
1 x ψ
2 chvarfv.1 x = y φ ψ
3 chvarfv.2 φ
4 2 biimpd x = y φ ψ
5 1 4 spimfv x φ ψ
6 5 3 mpg ψ