Description: If one case of an if- condition is a consequence of the other, the expression in dfifp4 can be shortened. (Contributed by Wolf Lammen, 18-Jun-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-ifp4impr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-ifpimpr | ||
2 | pm4.71 | ||
3 | 2 | biimpi | |
4 | 3 | orbi2d | |
5 | andir | ||
6 | 4 5 | bitr4di | |
7 | 1 6 | bitrd |