ifpbi3

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

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

Step	Hyp	Ref	Expression
1		imbi2	$⊢ (φ \leftrightarrow ψ) \to ((\neg χ \to φ) \leftrightarrow (\neg χ \to ψ))$
2	1	anbi2d	$⊢ (φ \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