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	⊢ ( 𝐴 ≠ 𝐵 → ( if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqif	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) ↔ ( ( 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) ∨ ( ¬ 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) ) )
2		ifnetrue	⊢ ( ( 𝐴 ≠ 𝐵 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) → 𝜑 )
3	2	adantrl	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) ) → 𝜑 )
4		simprl	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) ) → 𝜓 )
5	3 4	2thd	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) ) → ( 𝜑 ↔ 𝜓 ) )
6		ifnefals	⊢ ( ( 𝐴 ≠ 𝐵 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) → ¬ 𝜑 )
7	6	adantrl	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ¬ 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) ) → ¬ 𝜑 )
8		simprl	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ¬ 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) ) → ¬ 𝜓 )
9	7 8	2falsed	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ¬ 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) ) → ( 𝜑 ↔ 𝜓 ) )
10	5 9	jaodan	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ( 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ) ∨ ( ¬ 𝜓 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) ) ) → ( 𝜑 ↔ 𝜓 ) )
11	1 10	sylan2b	⊢ ( ( 𝐴 ≠ 𝐵 ∧ if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) ) → ( 𝜑 ↔ 𝜓 ) )
12		ifbi	⊢ ( ( 𝜑 ↔ 𝜓 ) → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) )
13	12	adantl	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝜑 ↔ 𝜓 ) ) → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) )
14	11 13	impbida	⊢ ( 𝐴 ≠ 𝐵 → ( if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐴 , 𝐵 ) ↔ ( 𝜑 ↔ 𝜓 ) ) )