Metamath Proof Explorer

Theorem 3optocl

Description: Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995)

Ref Expression
Hypotheses 3optocl.1 
|- R = ( D X. F )
3optocl.2 
|- ( <. x , y >. = A -> ( ph <-> ps ) )
3optocl.3 
|- ( <. z , w >. = B -> ( ps <-> ch ) )
3optocl.4 
|- ( <. v , u >. = C -> ( ch <-> th ) )
3optocl.5 
|- ( ( ( x e. D /\ y e. F ) /\ ( z e. D /\ w e. F ) /\ ( v e. D /\ u e. F ) ) -> ph )
Assertion 3optocl 
|- ( ( A e. R /\ B e. R /\ C e. R ) -> th )

Proof

Step Hyp Ref Expression
1 3optocl.1 
 |-  R = ( D X. F )
2 3optocl.2 
 |-  ( <. x , y >. = A -> ( ph <-> ps ) )
3 3optocl.3 
 |-  ( <. z , w >. = B -> ( ps <-> ch ) )
4 3optocl.4 
 |-  ( <. v , u >. = C -> ( ch <-> th ) )
5 3optocl.5 
 |-  ( ( ( x e. D /\ y e. F ) /\ ( z e. D /\ w e. F ) /\ ( v e. D /\ u e. F ) ) -> ph )
6 4 imbi2d 
 |-  ( <. v , u >. = C -> ( ( ( A e. R /\ B e. R ) -> ch ) <-> ( ( A e. R /\ B e. R ) -> th ) ) )
7 2 imbi2d 
 |-  ( <. x , y >. = A -> ( ( ( v e. D /\ u e. F ) -> ph ) <-> ( ( v e. D /\ u e. F ) -> ps ) ) )
8 3 imbi2d 
 |-  ( <. z , w >. = B -> ( ( ( v e. D /\ u e. F ) -> ps ) <-> ( ( v e. D /\ u e. F ) -> ch ) ) )
9 5 3expia 
 |-  ( ( ( x e. D /\ y e. F ) /\ ( z e. D /\ w e. F ) ) -> ( ( v e. D /\ u e. F ) -> ph ) )
10 1 7 8 9 2optocl 
 |-  ( ( A e. R /\ B e. R ) -> ( ( v e. D /\ u e. F ) -> ch ) )
11 10 com12 
 |-  ( ( v e. D /\ u e. F ) -> ( ( A e. R /\ B e. R ) -> ch ) )
12 1 6 11 optocl 
 |-  ( C e. R -> ( ( A e. R /\ B e. R ) -> th ) )
13 12 impcom 
 |-  ( ( ( A e. R /\ B e. R ) /\ C e. R ) -> th )
14 13 3impa 
 |-  ( ( A e. R /\ B e. R /\ C e. R ) -> th )