Step |
Hyp |
Ref |
Expression |
1 |
|
ifid |
|- if ( A <_ B , B , B ) = B |
2 |
|
xrletri3 |
|- ( ( B e. RR* /\ A e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) ) |
3 |
2
|
ancoms |
|- ( ( A e. RR* /\ B e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) ) |
4 |
3
|
biimpar |
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( B <_ A /\ A <_ B ) ) -> B = A ) |
5 |
4
|
anassrs |
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) /\ A <_ B ) -> B = A ) |
6 |
5
|
ifeq1da |
|- ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) -> if ( A <_ B , B , B ) = if ( A <_ B , A , B ) ) |
7 |
6
|
3impa |
|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , B , B ) = if ( A <_ B , A , B ) ) |
8 |
1 7
|
syl5reqr |
|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , A , B ) = B ) |