Theorem vtocl3

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)

	Ref	Expression
Hypotheses	vtocl3.1	|- A e. _V
	vtocl3.2	|- B e. _V
	vtocl3.3	|- C e. _V
	vtocl3.4	|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
	vtocl3.5	|- ph
Assertion	vtocl3	|- ps

Proof

Step	Hyp	Ref	Expression
1		vtocl3.1	|- A e. _V
2		vtocl3.2	|- B e. _V
3		vtocl3.3	|- C e. _V
4		vtocl3.4	|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
5		vtocl3.5	|- ph
6	5	a1i	|- ( z = C -> ph )
7	4	3expa	|- ( ( ( x = A /\ y = B ) /\ z = C ) -> ( ph <-> ps ) )
8	7	pm5.74da	|- ( ( x = A /\ y = B ) -> ( ( z = C -> ph ) <-> ( z = C -> ps ) ) )
9	1 2 8 6	vtocl2	|- ( z = C -> ps )
10	6 9	2thd	|- ( z = C -> ( ph <-> ps ) )
11	3 10 5	vtocl	|- ps