Metamath Proof Explorer

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	$⊢ (χ \to ψ) \to (if- (φ, ψ, χ) \leftrightarrow ((φ \lor χ) \land ψ))$

Proof

Step	Hyp	Ref	Expression
1		wl-ifpimpr	$⊢ (χ \to ψ) \to (if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor χ))$
2		pm4.71	$⊢ (χ \to ψ) \leftrightarrow (χ \leftrightarrow (χ \land ψ))$
3	2	biimpi	$⊢ (χ \to ψ) \to (χ \leftrightarrow (χ \land ψ))$
4	3	orbi2d	$⊢ (χ \to ψ) \to (((φ \land ψ) \lor χ) \leftrightarrow ((φ \land ψ) \lor (χ \land ψ)))$
5		andir	$⊢ ((φ \lor χ) \land ψ) \leftrightarrow ((φ \land ψ) \lor (χ \land ψ))$
6	4 5	bitr4di	$⊢ (χ \to ψ) \to (((φ \land ψ) \lor χ) \leftrightarrow ((φ \lor χ) \land ψ))$
7	1 6	bitrd	$⊢ (χ \to ψ) \to (if- (φ, ψ, χ) \leftrightarrow ((φ \lor χ) \land ψ))$