ifpimimb

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

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

Proof

Step	Hyp	Ref	Expression
1		dfifp2	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \leftrightarrow ((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ)))$
2		imor	$⊢ (φ \to (ψ \to χ)) \leftrightarrow (\neg φ \lor (ψ \to χ))$
3		pm4.8	$⊢ (φ \to \neg φ) \leftrightarrow \neg φ$
4	3	bicomi	$⊢ \neg φ \leftrightarrow (φ \to \neg φ)$
5	4	orbi1i	$⊢ (\neg φ \lor (ψ \to χ)) \leftrightarrow ((φ \to \neg φ) \lor (ψ \to χ))$
6		id	$⊢ φ \to φ$
7	6	orci	$⊢ ((φ \to φ) \lor (θ \to χ))$
8	7	biantru	$⊢ ((φ \to \neg φ) \lor (ψ \to χ)) \leftrightarrow (((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ)))$
9	2 5 8	3bitri	$⊢ (φ \to (ψ \to χ)) \leftrightarrow (((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ)))$
10		pm4.64	$⊢ (\neg φ \to (θ \to τ)) \leftrightarrow (φ \lor (θ \to τ))$
11		pm4.81	$⊢ (\neg φ \to φ) \leftrightarrow φ$
12	11	bicomi	$⊢ φ \leftrightarrow (\neg φ \to φ)$
13	12	orbi1i	$⊢ (φ \lor (θ \to τ)) \leftrightarrow ((\neg φ \to φ) \lor (θ \to τ))$
14	6	orci	$⊢ ((φ \to φ) \lor (ψ \to τ))$
15	14	biantrur	$⊢ ((\neg φ \to φ) \lor (θ \to τ)) \leftrightarrow (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ)))$
16	10 13 15	3bitri	$⊢ (\neg φ \to (θ \to τ)) \leftrightarrow (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ)))$
17	9 16	anbi12i	$⊢ ((φ \to (ψ \to χ)) \land (\neg φ \to (θ \to τ))) \leftrightarrow ((((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ))) \land (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ))))$
18		ifpim123g	$⊢ (if- (φ, ψ, θ) \to if- (φ, χ, τ)) \leftrightarrow ((((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ))) \land (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ))))$
19	18	bicomi	$⊢ ((((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ))) \land (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ)))) \leftrightarrow (if- (φ, ψ, θ) \to if- (φ, χ, τ))$
20	1 17 19	3bitri	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \leftrightarrow (if- (φ, ψ, θ) \to if- (φ, χ, τ))$

Metamath Proof Explorer

Theorem ifpimimb

Proof