Metamath Proof Explorer

Theorem ifpororb

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

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

Proof

Step	Hyp	Ref	Expression
1		dfifp2	$⊢ if- (φ, (ψ \lor χ), (θ \lor τ)) \leftrightarrow ((φ \to (ψ \lor χ)) \land (\neg φ \to (θ \lor τ)))$
2		df-or	$⊢ (ψ \lor χ) \leftrightarrow (\neg ψ \to χ)$
3	2	imbi2i	$⊢ (φ \to (ψ \lor χ)) \leftrightarrow (φ \to (\neg ψ \to χ))$
4		df-or	$⊢ (θ \lor τ) \leftrightarrow (\neg θ \to τ)$
5	4	imbi2i	$⊢ (\neg φ \to (θ \lor τ)) \leftrightarrow (\neg φ \to (\neg θ \to τ))$
6	3 5	anbi12i	$⊢ ((φ \to (ψ \lor χ)) \land (\neg φ \to (θ \lor τ))) \leftrightarrow ((φ \to (\neg ψ \to χ)) \land (\neg φ \to (\neg θ \to τ)))$
7		ifpimimb	$⊢ if- (φ, (\neg ψ \to χ), (\neg θ \to τ)) \leftrightarrow (if- (φ, \neg ψ, \neg θ) \to if- (φ, χ, τ))$
8		dfifp2	$⊢ if- (φ, (\neg ψ \to χ), (\neg θ \to τ)) \leftrightarrow ((φ \to (\neg ψ \to χ)) \land (\neg φ \to (\neg θ \to τ)))$
9		imor	$⊢ (if- (φ, \neg ψ, \neg θ) \to if- (φ, χ, τ)) \leftrightarrow (\neg if- (φ, \neg ψ, \neg θ) \lor if- (φ, χ, τ))$
10		ifpnot23d	$⊢ \neg if- (φ, \neg ψ, \neg θ) \leftrightarrow if- (φ, ψ, θ)$
11	10	orbi1i	$⊢ (\neg if- (φ, \neg ψ, \neg θ) \lor if- (φ, χ, τ)) \leftrightarrow (if- (φ, ψ, θ) \lor if- (φ, χ, τ))$
12	9 11	bitri	$⊢ (if- (φ, \neg ψ, \neg θ) \to if- (φ, χ, τ)) \leftrightarrow (if- (φ, ψ, θ) \lor if- (φ, χ, τ))$
13	7 8 12	3bitr3i	$⊢ ((φ \to (\neg ψ \to χ)) \land (\neg φ \to (\neg θ \to τ))) \leftrightarrow (if- (φ, ψ, θ) \lor if- (φ, χ, τ))$
14	1 6 13	3bitri	$⊢ if- (φ, (ψ \lor χ), (θ \lor τ)) \leftrightarrow (if- (φ, ψ, θ) \lor if- (φ, χ, τ))$