Metamath Proof Explorer


Theorem mdcompli

Description: A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of MaedaMaeda p. 4. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdcompl.1 A C
mdcompl.2 B C
Assertion mdcompli A 𝑀 B A A B 𝑀 B A B

Proof

Step Hyp Ref Expression
1 mdcompl.1 A C
2 mdcompl.2 B C
3 1 2 chincli A B C
4 3 mdoc1i A B 𝑀 A B
5 3 dmdoc2i A B 𝑀 * A B
6 ssid A B A B
7 1 2 chjcli A B C
8 7 chssii A B
9 3 chjoi A B A B =
10 8 9 sseqtrri A B A B A B
11 3 choccli A B C
12 3 11 1 2 mdslmd1i A B 𝑀 A B A B 𝑀 * A B A B A B A B A B A B A 𝑀 B A A B 𝑀 B A B
13 4 5 6 10 12 mp4an A 𝑀 B A A B 𝑀 B A B