Theorem elim2ifim

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

	Ref	Expression
Hypotheses	elim2if.1	⊢ ( if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = 𝐴 → ( 𝜒 ↔ 𝜃 ) )
	elim2if.2	⊢ ( if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = 𝐵 → ( 𝜒 ↔ 𝜏 ) )
	elim2if.3	⊢ ( if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = 𝐶 → ( 𝜒 ↔ 𝜂 ) )
	elim2ifim.1	⊢ ( 𝜑 → 𝜃 )
	elim2ifim.2	⊢ ( ( ¬ 𝜑 ∧ 𝜓 ) → 𝜏 )
	elim2ifim.3	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → 𝜂 )
Assertion	elim2ifim	⊢ 𝜒

Proof

Step	Hyp	Ref	Expression
1		elim2if.1	⊢ ( if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = 𝐴 → ( 𝜒 ↔ 𝜃 ) )
2		elim2if.2	⊢ ( if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = 𝐵 → ( 𝜒 ↔ 𝜏 ) )
3		elim2if.3	⊢ ( if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = 𝐶 → ( 𝜒 ↔ 𝜂 ) )
4		elim2ifim.1	⊢ ( 𝜑 → 𝜃 )
5		elim2ifim.2	⊢ ( ( ¬ 𝜑 ∧ 𝜓 ) → 𝜏 )
6		elim2ifim.3	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → 𝜂 )
7		exmid	⊢ ( 𝜑 ∨ ¬ 𝜑 )
8	4	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝜃 ) )
9		pm4.42	⊢ ( ¬ 𝜑 ↔ ( ( ¬ 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) )
10	5	ex	⊢ ( ¬ 𝜑 → ( 𝜓 → 𝜏 ) )
11	10	ancld	⊢ ( ¬ 𝜑 → ( 𝜓 → ( 𝜓 ∧ 𝜏 ) ) )
12	11	imp	⊢ ( ( ¬ 𝜑 ∧ 𝜓 ) → ( 𝜓 ∧ 𝜏 ) )
13	6	ex	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → 𝜂 ) )
14	13	ancld	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → ( ¬ 𝜓 ∧ 𝜂 ) ) )
15	14	imp	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ( ¬ 𝜓 ∧ 𝜂 ) )
16	12 15	orim12i	⊢ ( ( ( ¬ 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) → ( ( 𝜓 ∧ 𝜏 ) ∨ ( ¬ 𝜓 ∧ 𝜂 ) ) )
17	9 16	sylbi	⊢ ( ¬ 𝜑 → ( ( 𝜓 ∧ 𝜏 ) ∨ ( ¬ 𝜓 ∧ 𝜂 ) ) )
18	17	ancli	⊢ ( ¬ 𝜑 → ( ¬ 𝜑 ∧ ( ( 𝜓 ∧ 𝜏 ) ∨ ( ¬ 𝜓 ∧ 𝜂 ) ) ) )
19	8 18	orim12i	⊢ ( ( 𝜑 ∨ ¬ 𝜑 ) → ( ( 𝜑 ∧ 𝜃 ) ∨ ( ¬ 𝜑 ∧ ( ( 𝜓 ∧ 𝜏 ) ∨ ( ¬ 𝜓 ∧ 𝜂 ) ) ) ) )
20	7 19	ax-mp	⊢ ( ( 𝜑 ∧ 𝜃 ) ∨ ( ¬ 𝜑 ∧ ( ( 𝜓 ∧ 𝜏 ) ∨ ( ¬ 𝜓 ∧ 𝜂 ) ) ) )
21	1 2 3	elim2if	⊢ ( 𝜒 ↔ ( ( 𝜑 ∧ 𝜃 ) ∨ ( ¬ 𝜑 ∧ ( ( 𝜓 ∧ 𝜏 ) ∨ ( ¬ 𝜓 ∧ 𝜂 ) ) ) ) )
22	20 21	mpbir	⊢ 𝜒