# 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 )`