Theorem wl-ifp4impr

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

	Ref	Expression
Assertion	wl-ifp4impr	⊢ ( ( 𝜒 → 𝜓 ) → ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wl-ifpimpr	⊢ ( ( 𝜒 → 𝜓 ) → ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) ) )
2		pm4.71	⊢ ( ( 𝜒 → 𝜓 ) ↔ ( 𝜒 ↔ ( 𝜒 ∧ 𝜓 ) ) )
3	2	biimpi	⊢ ( ( 𝜒 → 𝜓 ) → ( 𝜒 ↔ ( 𝜒 ∧ 𝜓 ) ) )
4	3	orbi2d	⊢ ( ( 𝜒 → 𝜓 ) → ( ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ 𝜓 ) ) ) )
5		andir	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ∧ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ 𝜓 ) ) )
6	4 5	bitr4di	⊢ ( ( 𝜒 → 𝜓 ) → ( ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ 𝜓 ) ) )
7	1 6	bitrd	⊢ ( ( 𝜒 → 𝜓 ) → ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ 𝜓 ) ) )