Theorem ifnebib 32562

Description: The converse of ifbi 4548 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 4567	. . 3 ⊢ (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ ((𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) ∨ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)))
2		ifnetrue 32560	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) → 𝜑)
3	2	adantrl 716	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴)) → 𝜑)
4		simprl 771	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴)) → 𝜓)
5	3, 4	2thd 265	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴)) → (𝜑 ↔ 𝜓))
6		ifnefals 32561	. . . . . 6 ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵) → ¬ 𝜑)
7	6	adantrl 716	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)) → ¬ 𝜑)
8		simprl 771	. . . . 5 ⊢ ((𝐴 ≠ 𝐵 ∧ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)) → ¬ 𝜓)
9	7, 8	2falsed 376	. . . 4 ⊢ ((𝐴 ≠ 𝐵 ∧ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵)) → (𝜑 ↔ 𝜓))
10	5, 9	jaodan 960	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ ((𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) ∨ (¬ 𝜓 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵))) → (𝜑 ↔ 𝜓))
11	1, 10	sylan2b 594	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵)) → (𝜑 ↔ 𝜓))
12		ifbi 4548	. . 3 ⊢ ((𝜑 ↔ 𝜓) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
13	12	adantl 481	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ (𝜑 ↔ 𝜓)) → if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵))
14	11, 13	impbida 801	1 ⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1540   ≠ wne 2940  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-if 4526

This theorem is referenced by:  ply1moneq  33611