This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ifnebib

Description: The converse of ifbi holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Assertion ifnebib 
|- ( A =/= B -> ( if ( ph , A , B ) = if ( ps , A , B ) <-> ( ph <-> ps ) ) )

Proof

Step Hyp Ref Expression
1 eqif 
 |-  ( if ( ph , A , B ) = if ( ps , A , B ) <-> ( ( ps /\ if ( ph , A , B ) = A ) \/ ( -. ps /\ if ( ph , A , B ) = B ) ) )
2 ifnetrue 
 |-  ( ( A =/= B /\ if ( ph , A , B ) = A ) -> ph )
3 2 adantrl 
 |-  ( ( A =/= B /\ ( ps /\ if ( ph , A , B ) = A ) ) -> ph )
4 simprl 
 |-  ( ( A =/= B /\ ( ps /\ if ( ph , A , B ) = A ) ) -> ps )
5 3 4 2thd 
 |-  ( ( A =/= B /\ ( ps /\ if ( ph , A , B ) = A ) ) -> ( ph <-> ps ) )
6 ifnefals 
 |-  ( ( A =/= B /\ if ( ph , A , B ) = B ) -> -. ph )
7 6 adantrl 
 |-  ( ( A =/= B /\ ( -. ps /\ if ( ph , A , B ) = B ) ) -> -. ph )
8 simprl 
 |-  ( ( A =/= B /\ ( -. ps /\ if ( ph , A , B ) = B ) ) -> -. ps )
9 7 8 2falsed 
 |-  ( ( A =/= B /\ ( -. ps /\ if ( ph , A , B ) = B ) ) -> ( ph <-> ps ) )
10 5 9 jaodan 
 |-  ( ( A =/= B /\ ( ( ps /\ if ( ph , A , B ) = A ) \/ ( -. ps /\ if ( ph , A , B ) = B ) ) ) -> ( ph <-> ps ) )
11 1 10 sylan2b 
 |-  ( ( A =/= B /\ if ( ph , A , B ) = if ( ps , A , B ) ) -> ( ph <-> ps ) )
12 ifbi 
 |-  ( ( ph <-> ps ) -> if ( ph , A , B ) = if ( ps , A , B ) )
13 12 adantl 
 |-  ( ( A =/= B /\ ( ph <-> ps ) ) -> if ( ph , A , B ) = if ( ps , A , B ) )
14 11 13 impbida 
 |-  ( A =/= B -> ( if ( ph , A , B ) = if ( ps , A , B ) <-> ( ph <-> ps ) ) )