ifpbi23

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

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

Step	Hyp	Ref	Expression
1		simpl	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (φ \leftrightarrow ψ)$
2	1	imbi2d	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to ((τ \to φ) \leftrightarrow (τ \to ψ))$
3		simpr	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (χ \leftrightarrow θ)$
4	3	imbi2d	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to ((\neg τ \to χ) \leftrightarrow (\neg τ \to θ))$
5	2 4	anbi12d	$⊢ ((φ \leftrightarrow ψ) \land (χ \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 ψ) \land (χ \leftrightarrow θ)) \to (if- (τ, φ, χ) \leftrightarrow if- (τ, ψ, θ))$

Metamath Proof Explorer