ifpbi1

Description: Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020)

		Ref	Expression
	Assertion	ifpbi1	$⊢ (φ \leftrightarrow ψ) \to (if- (φ, χ, θ) \leftrightarrow if- (ψ, χ, θ))$

Step	Hyp	Ref	Expression
1		imbi1	$⊢ (φ \leftrightarrow ψ) \to ((φ \to χ) \leftrightarrow (ψ \to χ))$
2		notbi	$⊢ (φ \leftrightarrow ψ) \leftrightarrow (\neg φ \leftrightarrow \neg ψ)$
3	2	biimpi	$⊢ (φ \leftrightarrow ψ) \to (\neg φ \leftrightarrow \neg ψ)$
4	3	imbi1d	$⊢ (φ \leftrightarrow ψ) \to ((\neg φ \to θ) \leftrightarrow (\neg ψ \to θ))$
5	1 4	anbi12d	$⊢ (φ \leftrightarrow ψ) \to (((φ \to χ) \land (\neg φ \to θ)) \leftrightarrow ((ψ \to χ) \land (\neg ψ \to θ)))$
6		dfifp2	$⊢ if- (φ, χ, θ) \leftrightarrow ((φ \to χ) \land (\neg φ \to θ))$
7		dfifp2	$⊢ if- (ψ, χ, θ) \leftrightarrow ((ψ \to χ) \land (\neg ψ \to θ))$
8	5 6 7	3bitr4g	$⊢ (φ \leftrightarrow ψ) \to (if- (φ, χ, θ) \leftrightarrow if- (ψ, χ, θ))$

Metamath Proof Explorer