Metamath Proof Explorer

Theorem wl-ifpimpr

Description: If one case of an if- condition is a consequence of the other, the expression in df-ifp can be shortened. (Contributed by Wolf Lammen, 12-Jun-2024)

Ref Expression
Assertion wl-ifpimpr ⊢ χ → ψ → if- φ ψ χ ↔ φ ∧ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 pm4.72 ⊢ χ → ψ ↔ ψ ↔ χ ∨ ψ
2 1 biimpi ⊢ χ → ψ → ψ ↔ χ ∨ ψ
3 orcom ⊢ χ ∨ ψ ↔ ψ ∨ χ
4 2 3 bitrdi ⊢ χ → ψ → ψ ↔ ψ ∨ χ
5 4 anbi2d ⊢ χ → ψ → φ ∧ ψ ↔ φ ∧ ψ ∨ χ
6 andi ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ
7 5 6 bitrdi ⊢ χ → ψ → φ ∧ ψ ↔ φ ∧ ψ ∨ φ ∧ χ
8 7 orbi1d ⊢ χ → ψ → φ ∧ ψ ∨ ¬ φ ∧ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ¬ φ ∧ χ
9 df-ifp ⊢ if- φ ψ χ ↔ φ ∧ ψ ∨ ¬ φ ∧ χ
10 biidd ⊢ φ → χ ↔ χ
11 biidd ⊢ ¬ φ → χ ↔ χ
12 10 11 cases ⊢ χ ↔ φ ∧ χ ∨ ¬ φ ∧ χ
13 12 orbi2i ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ¬ φ ∧ χ
14 orass ⊢ φ ∧ ψ ∨ φ ∧ χ ∨ ¬ φ ∧ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ¬ φ ∧ χ
15 13 14 bitr4i ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ¬ φ ∧ χ
16 8 9 15 3bitr4g ⊢ χ → ψ → if- φ ψ χ ↔ φ ∧ ψ ∨ χ