ifpbi2

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

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

Step	Hyp	Ref	Expression
1		imbi2	$⊢ (φ \leftrightarrow ψ) \to ((χ \to φ) \leftrightarrow (χ \to ψ))$
2	1	anbi1d	$⊢ (φ \leftrightarrow ψ) \to (((χ \to φ) \land (\neg χ \to θ)) \leftrightarrow ((χ \to ψ) \land (\neg χ \to θ)))$
3		dfifp2	$⊢ if- (χ, φ, θ) \leftrightarrow ((χ \to φ) \land (\neg χ \to θ))$
4		dfifp2	$⊢ if- (χ, ψ, θ) \leftrightarrow ((χ \to ψ) \land (\neg χ \to θ))$
5	2 3 4	3bitr4g	$⊢ (φ \leftrightarrow ψ) \to (if- (χ, φ, θ) \leftrightarrow if- (χ, ψ, θ))$

Metamath Proof Explorer