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

Metamath Proof Explorer

Theorem vtocl4gaOLD

Description: Obsolete version of vtocl4ga as of 31-May-2025. (Contributed by AV, 22-Jan-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtocl4ga.1 
|- ( x = A -> ( ph <-> ps ) )
vtocl4ga.2 
|- ( y = B -> ( ps <-> ch ) )
vtocl4ga.3 
|- ( z = C -> ( ch <-> rh ) )
vtocl4ga.4 
|- ( w = D -> ( rh <-> th ) )
vtocl4ga.5 
|- ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ph )
Assertion vtocl4gaOLD 
|- ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th )

Proof

Step Hyp Ref Expression
1 vtocl4ga.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 vtocl4ga.2 
 |-  ( y = B -> ( ps <-> ch ) )
3 vtocl4ga.3 
 |-  ( z = C -> ( ch <-> rh ) )
4 vtocl4ga.4 
 |-  ( w = D -> ( rh <-> th ) )
5 vtocl4ga.5 
 |-  ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ph )
6 eleq1 
 |-  ( x = A -> ( x e. Q <-> A e. Q ) )
7 6 anbi1d 
 |-  ( x = A -> ( ( x e. Q /\ y e. R ) <-> ( A e. Q /\ y e. R ) ) )
8 7 anbi1d 
 |-  ( x = A -> ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) <-> ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) ) )
9 8 1 imbi12d 
 |-  ( x = A -> ( ( ( ( x e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ph ) <-> ( ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ps ) ) )
10 eleq1 
 |-  ( y = B -> ( y e. R <-> B e. R ) )
11 10 anbi2d 
 |-  ( y = B -> ( ( A e. Q /\ y e. R ) <-> ( A e. Q /\ B e. R ) ) )
12 11 anbi1d 
 |-  ( y = B -> ( ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) <-> ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) ) )
13 12 2 imbi12d 
 |-  ( y = B -> ( ( ( ( A e. Q /\ y e. R ) /\ ( z e. S /\ w e. T ) ) -> ps ) <-> ( ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) -> ch ) ) )
14 eleq1 
 |-  ( z = C -> ( z e. S <-> C e. S ) )
15 14 anbi1d 
 |-  ( z = C -> ( ( z e. S /\ w e. T ) <-> ( C e. S /\ w e. T ) ) )
16 15 anbi2d 
 |-  ( z = C -> ( ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) <-> ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) ) )
17 16 3 imbi12d 
 |-  ( z = C -> ( ( ( ( A e. Q /\ B e. R ) /\ ( z e. S /\ w e. T ) ) -> ch ) <-> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) -> rh ) ) )
18 eleq1 
 |-  ( w = D -> ( w e. T <-> D e. T ) )
19 18 anbi2d 
 |-  ( w = D -> ( ( C e. S /\ w e. T ) <-> ( C e. S /\ D e. T ) ) )
20 19 anbi2d 
 |-  ( w = D -> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) <-> ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) ) )
21 20 4 imbi12d 
 |-  ( w = D -> ( ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ w e. T ) ) -> rh ) <-> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th ) ) )
22 9 13 17 21 5 vtocl4g 
 |-  ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th ) )
23 22 pm2.43i 
 |-  ( ( ( A e. Q /\ B e. R ) /\ ( C e. S /\ D e. T ) ) -> th )