elim2ifim

Description: Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypotheses	elim2if.1	$⊢ if (φ, A, if (ψ, B, C)) = A \to (χ \leftrightarrow θ)$
	elim2if.2	$⊢ if (φ, A, if (ψ, B, C)) = B \to (χ \leftrightarrow τ)$
	elim2if.3	$⊢ if (φ, A, if (ψ, B, C)) = C \to (χ \leftrightarrow η)$
	elim2ifim.1	$⊢ φ \to θ$
	elim2ifim.2	$⊢ (\neg φ \land ψ) \to τ$
	elim2ifim.3	$⊢ (\neg φ \land \neg ψ) \to η$
Assertion	elim2ifim	$⊢ χ$

Step	Hyp	Ref	Expression
1		elim2if.1	$⊢ if (φ, A, if (ψ, B, C)) = A \to (χ \leftrightarrow θ)$
2		elim2if.2	$⊢ if (φ, A, if (ψ, B, C)) = B \to (χ \leftrightarrow τ)$
3		elim2if.3	$⊢ if (φ, A, if (ψ, B, C)) = C \to (χ \leftrightarrow η)$
4		elim2ifim.1	$⊢ φ \to θ$
5		elim2ifim.2	$⊢ (\neg φ \land ψ) \to τ$
6		elim2ifim.3	$⊢ (\neg φ \land \neg ψ) \to η$
7		exmid	$⊢ (φ \lor \neg φ)$
8	4	ancli	$⊢ φ \to (φ \land θ)$
9		pm4.42	$⊢ \neg φ \leftrightarrow ((\neg φ \land ψ) \lor (\neg φ \land \neg ψ))$
10	5	ex	$⊢ \neg φ \to (ψ \to τ)$
11	10	ancld	$⊢ \neg φ \to (ψ \to (ψ \land τ))$
12	11	imp	$⊢ (\neg φ \land ψ) \to (ψ \land τ)$
13	6	ex	$⊢ \neg φ \to (\neg ψ \to η)$
14	13	ancld	$⊢ \neg φ \to (\neg ψ \to (\neg ψ \land η))$
15	14	imp	$⊢ (\neg φ \land \neg ψ) \to (\neg ψ \land η)$
16	12 15	orim12i	$⊢ ((\neg φ \land ψ) \lor (\neg φ \land \neg ψ)) \to ((ψ \land τ) \lor (\neg ψ \land η))$
17	9 16	sylbi	$⊢ \neg φ \to ((ψ \land τ) \lor (\neg ψ \land η))$
18	17	ancli	$⊢ \neg φ \to (\neg φ \land ((ψ \land τ) \lor (\neg ψ \land η)))$
19	8 18	orim12i	$⊢ (φ \lor \neg φ) \to ((φ \land θ) \lor (\neg φ \land ((ψ \land τ) \lor (\neg ψ \land η))))$
20	7 19	ax-mp	$⊢ ((φ \land θ) \lor (\neg φ \land ((ψ \land τ) \lor (\neg ψ \land η))))$
21	1 2 3	elim2if	$⊢ χ \leftrightarrow ((φ \land θ) \lor (\neg φ \land ((ψ \land τ) \lor (\neg ψ \land η))))$
22	20 21	mpbir	$⊢ χ$

Metamath Proof Explorer