Metamath Proof Explorer


Theorem vtoclfOLD

Description: Obsolete version of vtoclf as of 26-Jan-2025. (Contributed by NM, 30-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtoclf.1 x ψ
vtoclf.2 A V
vtoclf.3 x = A φ ψ
vtoclf.4 φ
Assertion vtoclfOLD ψ

Proof

Step Hyp Ref Expression
1 vtoclf.1 x ψ
2 vtoclf.2 A V
3 vtoclf.3 x = A φ ψ
4 vtoclf.4 φ
5 2 isseti x x = A
6 3 biimpd x = A φ ψ
7 5 6 eximii x φ ψ
8 1 7 19.36i x φ ψ
9 8 4 mpg ψ