Theorem ifnebib 32572

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

Assertion

Ref	Expression
ifnebib	⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓)))

Proof of Theorem ifnebib

Step	Hyp	Ref	Expression
1		eqif 4589	. . 3 ⊢ (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ ((𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) ∨ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)))
2		ifnetrue 32570	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) → 𝜑)
3	2	adantrl 715	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴)) → 𝜑)
4		simprl 770	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴)) → 𝜓)
5	3, 4	2thd 265	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴)) → (𝜑 ↔ 𝜓))
6		ifnefals 32571	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵) → ¬ 𝜑)
7	6	adantrl 715	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)) → ¬ 𝜑)
8		simprl 770	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)) → ¬ 𝜓)
9	7, 8	2falsed 376	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)) → (𝜑 ↔ 𝜓))
10	5, 9	jaodan 958	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ ((𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) ∨ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵))) → (𝜑 ↔ 𝜓))
11	1, 10	sylan2b 593	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵)) → (𝜑 ↔ 𝜓))
12		ifbi 4570	. . 3 ⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
13	12	adantl 481	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜑 ↔ 𝜓)) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
14	11, 13	impbida 800	1 ⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   = wceq 1537   ≠ wne 2946  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-if 4549

This theorem is referenced by:  ply1moneq  33576