Description: Double adjoint. Theorem 3.11(iv) of Beran p. 106. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | adjadj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | adj2 | |
|
2 | dmadjrn | |
|
3 | adj1 | |
|
4 | 2 3 | syl3an1 | |
5 | 1 4 | eqtr2d | |
6 | 5 | 3expib | |
7 | 6 | ralrimivv | |
8 | dmadjrn | |
|
9 | dmadjop | |
|
10 | 2 8 9 | 3syl | |
11 | dmadjop | |
|
12 | hoeq1 | |
|
13 | 10 11 12 | syl2anc | |
14 | 7 13 | mpbid | |