This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 GG, 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