Description: Theorem *5.17 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 3-Jan-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | pm5.17 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom | |
|
2 | dfbi2 | |
|
3 | orcom | |
|
4 | df-or | |
|
5 | 3 4 | bitr2i | |
6 | imnan | |
|
7 | 5 6 | anbi12i | |
8 | 1 2 7 | 3bitrri | |