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

Proof

Step	Hyp	Ref	Expression
1		wl-ifpimpr	|- ( ( ch -> ps ) -> ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ch ) ) )
2		pm4.71	|- ( ( ch -> ps ) <-> ( ch <-> ( ch /\ ps ) ) )
3	2	biimpi	|- ( ( ch -> ps ) -> ( ch <-> ( ch /\ ps ) ) )
4	3	orbi2d	|- ( ( ch -> ps ) -> ( ( ( ph /\ ps ) \/ ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ps ) ) ) )
5		andir	|- ( ( ( ph \/ ch ) /\ ps ) <-> ( ( ph /\ ps ) \/ ( ch /\ ps ) ) )
6	4 5	bitr4di	|- ( ( ch -> ps ) -> ( ( ( ph /\ ps ) \/ ch ) <-> ( ( ph \/ ch ) /\ ps ) ) )
7	1 6	bitrd	|- ( ( ch -> ps ) -> ( if- ( ph , ps , ch ) <-> ( ( ph \/ ch ) /\ ps ) ) )