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	|- ( ( ch -> ps ) -> ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm4.72	|- ( ( ch -> ps ) <-> ( ps <-> ( ch \/ ps ) ) )
2	1	biimpi	|- ( ( ch -> ps ) -> ( ps <-> ( ch \/ ps ) ) )
3		orcom	|- ( ( ch \/ ps ) <-> ( ps \/ ch ) )
4	2 3	bitrdi	|- ( ( ch -> ps ) -> ( ps <-> ( ps \/ ch ) ) )
5	4	anbi2d	|- ( ( ch -> ps ) -> ( ( ph /\ ps ) <-> ( ph /\ ( ps \/ ch ) ) ) )
6		andi	|- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
7	5 6	bitrdi	|- ( ( ch -> ps ) -> ( ( ph /\ ps ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) ) )
8	7	orbi1d	|- ( ( ch -> ps ) -> ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( -. ph /\ ch ) ) ) )
9		df-ifp	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
10		biidd	|- ( ph -> ( ch <-> ch ) )
11		biidd	|- ( -. ph -> ( ch <-> ch ) )
12	10 11	cases	|- ( ch <-> ( ( ph /\ ch ) \/ ( -. ph /\ ch ) ) )
13	12	orbi2i	|- ( ( ( ph /\ ps ) \/ ch ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( -. ph /\ ch ) ) ) )
14		orass	|- ( ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( -. ph /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ ch ) \/ ( -. ph /\ ch ) ) ) )
15	13 14	bitr4i	|- ( ( ( ph /\ ps ) \/ ch ) <-> ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) \/ ( -. ph /\ ch ) ) )
16	8 9 15	3bitr4g	|- ( ( ch -> ps ) -> ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ch ) ) )