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 φ A B = if ψ A B ↔ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 eqif ⊢ if φ A B = if ψ A B ↔ ψ ∧ if φ A B = A ∨ ¬ ψ ∧ if φ A B = B
2 ifnetrue ⊢ A ≠ B ∧ if φ A B = A → φ
3 2 adantrl ⊢ A ≠ B ∧ ψ ∧ if φ A B = A → φ
4 simprl ⊢ A ≠ B ∧ ψ ∧ if φ A B = A → ψ
5 3 4 2thd ⊢ A ≠ B ∧ ψ ∧ if φ A B = A → φ ↔ ψ
6 ifnefals ⊢ A ≠ B ∧ if φ A B = B → ¬ φ
7 6 adantrl ⊢ A ≠ B ∧ ¬ ψ ∧ if φ A B = B → ¬ φ
8 simprl ⊢ A ≠ B ∧ ¬ ψ ∧ if φ A B = B → ¬ ψ
9 7 8 2falsed ⊢ A ≠ B ∧ ¬ ψ ∧ if φ A B = B → φ ↔ ψ
10 5 9 jaodan ⊢ A ≠ B ∧ ψ ∧ if φ A B = A ∨ ¬ ψ ∧ if φ A B = B → φ ↔ ψ
11 1 10 sylan2b ⊢ A ≠ B ∧ if φ A B = if ψ A B → φ ↔ ψ
12 ifbi ⊢ φ ↔ ψ → if φ A B = if ψ A B
13 12 adantl ⊢ A ≠ B ∧ φ ↔ ψ → if φ A B = if ψ A B
14 11 13 impbida ⊢ A ≠ B → if φ A B = if ψ A B ↔ φ ↔ ψ