# Metamath Proof Explorer

## Theorem mdi

Description: Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mdi
`|- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) )`

### Proof

Step Hyp Ref Expression
1 mdbr
` |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )`
2 1 biimpd
` |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B -> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )`
3 sseq1
` |-  ( x = C -> ( x C_ B <-> C C_ B ) )`
4 oveq1
` |-  ( x = C -> ( x vH A ) = ( C vH A ) )`
5 4 ineq1d
` |-  ( x = C -> ( ( x vH A ) i^i B ) = ( ( C vH A ) i^i B ) )`
6 oveq1
` |-  ( x = C -> ( x vH ( A i^i B ) ) = ( C vH ( A i^i B ) ) )`
7 5 6 eqeq12d
` |-  ( x = C -> ( ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) <-> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) ) )`
8 3 7 imbi12d
` |-  ( x = C -> ( ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) <-> ( C C_ B -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) ) ) )`
9 8 rspcv
` |-  ( C e. CH -> ( A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) -> ( C C_ B -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) ) ) )`
10 2 9 sylan9
` |-  ( ( ( A e. CH /\ B e. CH ) /\ C e. CH ) -> ( A MH B -> ( C C_ B -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) ) ) )`
11 10 3impa
` |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A MH B -> ( C C_ B -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) ) ) )`
12 11 imp32
` |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) )`