ifpbi13

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

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

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

Metamath Proof Explorer