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

Proof

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