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(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓))) |