ifpbibib

Description: Factor conditional logic operator over biconditional in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		dfifp2	$⊢ if- (φ, (ψ \leftrightarrow χ), (θ \leftrightarrow τ)) \leftrightarrow ((φ \to (ψ \leftrightarrow χ)) \land (\neg φ \to (θ \leftrightarrow τ)))$
2		dfbi2	$⊢ (ψ \leftrightarrow χ) \leftrightarrow ((ψ \to χ) \land (χ \to ψ))$
3	2	imbi2i	$⊢ (φ \to (ψ \leftrightarrow χ)) \leftrightarrow (φ \to ((ψ \to χ) \land (χ \to ψ)))$
4		jcab	$⊢ (φ \to ((ψ \to χ) \land (χ \to ψ))) \leftrightarrow ((φ \to (ψ \to χ)) \land (φ \to (χ \to ψ)))$
5	3 4	bitri	$⊢ (φ \to (ψ \leftrightarrow χ)) \leftrightarrow ((φ \to (ψ \to χ)) \land (φ \to (χ \to ψ)))$
6		dfbi2	$⊢ (θ \leftrightarrow τ) \leftrightarrow ((θ \to τ) \land (τ \to θ))$
7	6	imbi2i	$⊢ (\neg φ \to (θ \leftrightarrow τ)) \leftrightarrow (\neg φ \to ((θ \to τ) \land (τ \to θ)))$
8		jcab	$⊢ (\neg φ \to ((θ \to τ) \land (τ \to θ))) \leftrightarrow ((\neg φ \to (θ \to τ)) \land (\neg φ \to (τ \to θ)))$
9	7 8	bitri	$⊢ (\neg φ \to (θ \leftrightarrow τ)) \leftrightarrow ((\neg φ \to (θ \to τ)) \land (\neg φ \to (τ \to θ)))$
10	5 9	anbi12i	$⊢ ((φ \to (ψ \leftrightarrow χ)) \land (\neg φ \to (θ \leftrightarrow τ))) \leftrightarrow (((φ \to (ψ \to χ)) \land (φ \to (χ \to ψ))) \land ((\neg φ \to (θ \to τ)) \land (\neg φ \to (τ \to θ))))$
11		an4	$⊢ (((φ \to (ψ \to χ)) \land (φ \to (χ \to ψ))) \land ((\neg φ \to (θ \to τ)) \land (\neg φ \to (τ \to θ)))) \leftrightarrow (((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ))) \land ((φ \to (χ \to ψ)) \land (\neg φ \to (τ \to θ))))$
12	10 11	bitri	$⊢ ((φ \to (ψ \leftrightarrow χ)) \land (\neg φ \to (θ \leftrightarrow τ))) \leftrightarrow (((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ))) \land ((φ \to (χ \to ψ)) \land (\neg φ \to (τ \to θ))))$
13		dfifp2	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \leftrightarrow ((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ)))$
14		ifpimimb	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \leftrightarrow (if- (φ, ψ, θ) \to if- (φ, χ, τ))$
15	13 14	bitr3i	$⊢ ((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ))) \leftrightarrow (if- (φ, ψ, θ) \to if- (φ, χ, τ))$
16		dfifp2	$⊢ if- (φ, (χ \to ψ), (τ \to θ)) \leftrightarrow ((φ \to (χ \to ψ)) \land (\neg φ \to (τ \to θ)))$
17		ifpimimb	$⊢ if- (φ, (χ \to ψ), (τ \to θ)) \leftrightarrow (if- (φ, χ, τ) \to if- (φ, ψ, θ))$
18	16 17	bitr3i	$⊢ ((φ \to (χ \to ψ)) \land (\neg φ \to (τ \to θ))) \leftrightarrow (if- (φ, χ, τ) \to if- (φ, ψ, θ))$
19	15 18	anbi12i	$⊢ (((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ))) \land ((φ \to (χ \to ψ)) \land (\neg φ \to (τ \to θ)))) \leftrightarrow ((if- (φ, ψ, θ) \to if- (φ, χ, τ)) \land (if- (φ, χ, τ) \to if- (φ, ψ, θ)))$
20		dfbi2	$⊢ (if- (φ, ψ, θ) \leftrightarrow if- (φ, χ, τ)) \leftrightarrow ((if- (φ, ψ, θ) \to if- (φ, χ, τ)) \land (if- (φ, χ, τ) \to if- (φ, ψ, θ)))$
21	19 20	bitr4i	$⊢ (((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ))) \land ((φ \to (χ \to ψ)) \land (\neg φ \to (τ \to θ)))) \leftrightarrow (if- (φ, ψ, θ) \leftrightarrow if- (φ, χ, τ))$
22	1 12 21	3bitri	$⊢ if- (φ, (ψ \leftrightarrow χ), (θ \leftrightarrow τ)) \leftrightarrow (if- (φ, ψ, θ) \leftrightarrow if- (φ, χ, τ))$

Metamath Proof Explorer

Theorem ifpbibib

Proof