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

Metamath Proof Explorer

Theorem vtocl2d

Description: Implicit substitution of two classes for two setvar variables. (Contributed by Thierry Arnoux, 25-Aug-2020) (Revised by BTernaryTau, 19-Oct-2023)

Ref Expression
Hypotheses vtocl2d.a 
|- ( ph -> A e. V )
vtocl2d.b 
|- ( ph -> B e. W )
vtocl2d.1 
|- ( ( x = A /\ y = B ) -> ( ps <-> ch ) )
vtocl2d.3 
|- ( ph -> ps )
Assertion vtocl2d 
|- ( ph -> ch )

Proof

Step Hyp Ref Expression
1 vtocl2d.a 
 |-  ( ph -> A e. V )
2 vtocl2d.b 
 |-  ( ph -> B e. W )
3 vtocl2d.1 
 |-  ( ( x = A /\ y = B ) -> ( ps <-> ch ) )
4 vtocl2d.3 
 |-  ( ph -> ps )
5 4 adantr 
 |-  ( ( ph /\ y = B ) -> ps )
6 3 adantll 
 |-  ( ( ( ph /\ x = A ) /\ y = B ) -> ( ps <-> ch ) )
7 6 pm5.74da 
 |-  ( ( ph /\ x = A ) -> ( ( y = B -> ps ) <-> ( y = B -> ch ) ) )
8 4 a1d 
 |-  ( ph -> ( y = B -> ps ) )
9 1 7 8 vtocld 
 |-  ( ph -> ( y = B -> ch ) )
10 9 imp 
 |-  ( ( ph /\ y = B ) -> ch )
11 5 10 2thd 
 |-  ( ( ph /\ y = B ) -> ( ps <-> ch ) )
12 2 11 4 vtocld 
 |-  ( ph -> ch )