Metamath Proof Explorer

Theorem ifpbi123dOLD

Description: Obsolete version of ifpbi123d as of 17-Apr-2024. (Contributed by AV, 30-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	ifpbi123d.1	$⊢ φ \to (ψ \leftrightarrow τ)$
		ifpbi123d.2	$⊢ φ \to (χ \leftrightarrow η)$
		ifpbi123d.3	$⊢ φ \to (θ \leftrightarrow ζ)$
	Assertion	ifpbi123dOLD	$⊢ φ \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	anbi12d	$⊢ φ \to ((ψ \land χ) \leftrightarrow (τ \land η))$
5	1	notbid	$⊢ φ \to (\neg ψ \leftrightarrow \neg τ)$
6	5 3	anbi12d	$⊢ φ \to ((\neg ψ \land θ) \leftrightarrow (\neg τ \land ζ))$
7	4 6	orbi12d	$⊢ φ \to (((ψ \land χ) \lor (\neg ψ \land θ)) \leftrightarrow ((τ \land η) \lor (\neg τ \land ζ)))$
8		df-ifp	$⊢ if- (ψ, χ, θ) \leftrightarrow ((ψ \land χ) \lor (\neg ψ \land θ))$
9		df-ifp	$⊢ if- (τ, η, ζ) \leftrightarrow ((τ \land η) \lor (\neg τ \land ζ))$
10	7 8 9	3bitr4g	$⊢ φ \to (if- (ψ, χ, θ) \leftrightarrow if- (τ, η, ζ))$