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

Metamath Proof Explorer

Theorem vtocl3gaOLD

Description: Obsolete version of vtocl3ga as of 31-May-2025. (Contributed by NM, 20-Aug-1995) Reduce axiom usage. (Revised by GG, 3-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtocl3ga.1 
|- ( x = A -> ( ph <-> ps ) )
vtocl3ga.2 
|- ( y = B -> ( ps <-> ch ) )
vtocl3ga.3 
|- ( z = C -> ( ch <-> th ) )
vtocl3ga.4 
|- ( ( x e. D /\ y e. R /\ z e. S ) -> ph )
Assertion vtocl3gaOLD 
|- ( ( A e. D /\ B e. R /\ C e. S ) -> th )

Proof

Step Hyp Ref Expression
1 vtocl3ga.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 vtocl3ga.2 
 |-  ( y = B -> ( ps <-> ch ) )
3 vtocl3ga.3 
 |-  ( z = C -> ( ch <-> th ) )
4 vtocl3ga.4 
 |-  ( ( x e. D /\ y e. R /\ z e. S ) -> ph )
5 eleq1 
 |-  ( x = A -> ( x e. D <-> A e. D ) )
6 5 3anbi1d 
 |-  ( x = A -> ( ( x e. D /\ y e. R /\ z e. S ) <-> ( A e. D /\ y e. R /\ z e. S ) ) )
7 6 1 imbi12d 
 |-  ( x = A -> ( ( ( x e. D /\ y e. R /\ z e. S ) -> ph ) <-> ( ( A e. D /\ y e. R /\ z e. S ) -> ps ) ) )
8 eleq1 
 |-  ( y = B -> ( y e. R <-> B e. R ) )
9 8 3anbi2d 
 |-  ( y = B -> ( ( A e. D /\ y e. R /\ z e. S ) <-> ( A e. D /\ B e. R /\ z e. S ) ) )
10 9 2 imbi12d 
 |-  ( y = B -> ( ( ( A e. D /\ y e. R /\ z e. S ) -> ps ) <-> ( ( A e. D /\ B e. R /\ z e. S ) -> ch ) ) )
11 eleq1 
 |-  ( z = C -> ( z e. S <-> C e. S ) )
12 11 3anbi3d 
 |-  ( z = C -> ( ( A e. D /\ B e. R /\ z e. S ) <-> ( A e. D /\ B e. R /\ C e. S ) ) )
13 12 3 imbi12d 
 |-  ( z = C -> ( ( ( A e. D /\ B e. R /\ z e. S ) -> ch ) <-> ( ( A e. D /\ B e. R /\ C e. S ) -> th ) ) )
14 7 10 13 4 vtocl3g 
 |-  ( ( A e. D /\ B e. R /\ C e. S ) -> ( ( A e. D /\ B e. R /\ C e. S ) -> th ) )
15 14 pm2.43i 
 |-  ( ( A e. D /\ B e. R /\ C e. S ) -> th )