Metamath Proof Explorer

Theorem vtoclgOLD

Description: Obsolete version of vtoclg as of 20-Apr-2024. (Contributed by NM, 17-Apr-1995) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses vtoclgOLD.1 x = A φ ψ
vtoclgOLD.2 φ
Assertion vtoclgOLD A V ψ


Step Hyp Ref Expression
1 vtoclgOLD.1 x = A φ ψ
2 vtoclgOLD.2 φ
3 nfv x ψ
4 3 1 2 vtoclg1f A V ψ