Metamath Proof Explorer


Theorem dmdi

Description: Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion dmdi ACBCCCA𝑀*BBCCAB=CAB

Proof

Step Hyp Ref Expression
1 dmdbr ACBCA𝑀*BxCBxxAB=xAB
2 1 biimpd ACBCA𝑀*BxCBxxAB=xAB
3 sseq2 x=CBxBC
4 ineq1 x=CxA=CA
5 4 oveq1d x=CxAB=CAB
6 ineq1 x=CxAB=CAB
7 5 6 eqeq12d x=CxAB=xABCAB=CAB
8 3 7 imbi12d x=CBxxAB=xABBCCAB=CAB
9 8 rspcv CCxCBxxAB=xABBCCAB=CAB
10 2 9 sylan9 ACBCCCA𝑀*BBCCAB=CAB
11 10 3impa ACBCCCA𝑀*BBCCAB=CAB
12 11 imp32 ACBCCCA𝑀*BBCCAB=CAB