Description: When the branches are not equal, an "if" condition results in the first branch if and only if its condition is true. (Contributed by SN, 16-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | iftrueb | |- ( A =/= B -> ( if ( ph , A , B ) = A <-> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | necom | |- ( A =/= B <-> B =/= A ) |
|
| 2 | 1 | biimpi | |- ( A =/= B -> B =/= A ) |
| 3 | iffalse | |- ( -. ph -> if ( ph , A , B ) = B ) |
|
| 4 | 3 | neeq1d | |- ( -. ph -> ( if ( ph , A , B ) =/= A <-> B =/= A ) ) |
| 5 | 2 4 | syl5ibrcom | |- ( A =/= B -> ( -. ph -> if ( ph , A , B ) =/= A ) ) |
| 6 | 5 | necon4bd | |- ( A =/= B -> ( if ( ph , A , B ) = A -> ph ) ) |
| 7 | iftrue | |- ( ph -> if ( ph , A , B ) = A ) |
|
| 8 | 6 7 | impbid1 | |- ( A =/= B -> ( if ( ph , A , B ) = A <-> ph ) ) |