Metamath Proof Explorer

Theorem 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		simpr	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (χ \leftrightarrow θ)$
3	1 2	ifpbi23d	$⊢ ((φ \leftrightarrow ψ) \land (χ \leftrightarrow θ)) \to (if- (τ, φ, χ) \leftrightarrow if- (τ, ψ, θ))$