ifpbi12

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

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

Step	Hyp	Ref	Expression
1		imbi12	$⊢ (φ \leftrightarrow ψ) \to ((χ \leftrightarrow θ) \to ((φ \to χ) \leftrightarrow (ψ \to θ)))$
2	1	imp	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to ((φ \to χ) \leftrightarrow (ψ \to θ))$
3		simpl	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (φ \leftrightarrow ψ)$
4	3	notbid	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (\neg φ \leftrightarrow \neg ψ)$
5	4	imbi1d	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to ((\neg φ \to τ) \leftrightarrow (\neg ψ \to τ))$
6	2 5	anbi12d	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (((φ \to χ) \land (\neg φ \to τ)) \leftrightarrow ((ψ \to θ) \land (\neg ψ \to τ)))$
7		dfifp2	$⊢ if- (φ, χ, τ) \leftrightarrow ((φ \to χ) \land (\neg φ \to τ))$
8		dfifp2	$⊢ if- (ψ, θ, τ) \leftrightarrow ((ψ \to θ) \land (\neg ψ \to τ))$
9	6 7 8	3bitr4g	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (if- (φ, χ, τ) \leftrightarrow if- (ψ, θ, τ))$

Metamath Proof Explorer