Metamath Proof Explorer

Theorem ifpbi123d

Description: Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020) (Proof shortened by Wolf Lammen, 17-Apr-2024)

		Ref	Expression
	Hypotheses	ifpbi123d.1	$⊢ φ \to (ψ \leftrightarrow τ)$
		ifpbi123d.2	$⊢ φ \to (χ \leftrightarrow η)$
		ifpbi123d.3	$⊢ φ \to (θ \leftrightarrow ζ)$
	Assertion	ifpbi123d	$⊢ φ \to (if- (ψ, χ, θ) \leftrightarrow if- (τ, η, ζ))$

Proof

Step	Hyp	Ref	Expression
1		ifpbi123d.1	$⊢ φ \to (ψ \leftrightarrow τ)$
2		ifpbi123d.2	$⊢ φ \to (χ \leftrightarrow η)$
3		ifpbi123d.3	$⊢ φ \to (θ \leftrightarrow ζ)$
4	1 2	imbi12d	$⊢ φ \to ((ψ \to χ) \leftrightarrow (τ \to η))$
5	1 3	orbi12d	$⊢ φ \to ((ψ \lor θ) \leftrightarrow (τ \lor ζ))$
6	4 5	anbi12d	$⊢ φ \to (((ψ \to χ) \land (ψ \lor θ)) \leftrightarrow ((τ \to η) \land (τ \lor ζ)))$
7		dfifp3	$⊢ if- (ψ, χ, θ) \leftrightarrow ((ψ \to χ) \land (ψ \lor θ))$
8		dfifp3	$⊢ if- (τ, η, ζ) \leftrightarrow ((τ \to η) \land (τ \lor ζ))$
9	6 7 8	3bitr4g	$⊢ φ \to (if- (ψ, χ, θ) \leftrightarrow if- (τ, η, ζ))$