Metamath Proof Explorer


Theorem opthpr

Description: An unordered pair has the ordered pair property (compare opth ) under certain conditions. (Contributed by NM, 27-Mar-2007)

Ref Expression
Hypotheses preqr1.a A V
preqr1.b B V
preq12b.c C V
preq12b.d D V
Assertion opthpr A D A B = C D A = C B = D

Proof

Step Hyp Ref Expression
1 preqr1.a A V
2 preqr1.b B V
3 preq12b.c C V
4 preq12b.d D V
5 1 2 3 4 preq12b A B = C D A = C B = D A = D B = C
6 idd A D A = C B = D A = C B = D
7 df-ne A D ¬ A = D
8 pm2.21 ¬ A = D A = D B = C A = C B = D
9 7 8 sylbi A D A = D B = C A = C B = D
10 9 impd A D A = D B = C A = C B = D
11 6 10 jaod A D A = C B = D A = D B = C A = C B = D
12 orc A = C B = D A = C B = D A = D B = C
13 11 12 impbid1 A D A = C B = D A = D B = C A = C B = D
14 5 13 syl5bb A D A B = C D A = C B = D