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-φψχ↔φ∧ψ∨χ