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- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ 𝜒 ) ) )