Theorem vtocleOLD

Description: Obsolete version of vtocle as of 31-May-2025. (Contributed by NM, 9-Sep-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vtocle.1	|- A e. _V
	vtocle.2	|- ( x = A -> ph )
Assertion	vtocleOLD	|- ph

Proof

Step	Hyp	Ref	Expression
1		vtocle.1	|- A e. _V
2		vtocle.2	|- ( x = A -> ph )
3	2	vtocleg	|- ( A e. _V -> ph )
4	1 3	ax-mp	|- ph