Theorem exmid2

Description: An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019)

	Ref	Expression
Hypotheses	exmid2.1	⊢ ( ( 𝜓 ∧ 𝜑 ) → 𝜒 )
	exmid2.2	⊢ ( ( ¬ 𝜓 ∧ 𝜂 ) → 𝜒 )
Assertion	exmid2	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		exmid2.1	⊢ ( ( 𝜓 ∧ 𝜑 ) → 𝜒 )
2		exmid2.2	⊢ ( ( ¬ 𝜓 ∧ 𝜂 ) → 𝜒 )
3		simpl	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜑 )
4	3	anim2i	⊢ ( ( 𝜓 ∧ ( 𝜑 ∧ 𝜂 ) ) → ( 𝜓 ∧ 𝜑 ) )
5	4	ancoms	⊢ ( ( ( 𝜑 ∧ 𝜂 ) ∧ 𝜓 ) → ( 𝜓 ∧ 𝜑 ) )
6	5 1	syl	⊢ ( ( ( 𝜑 ∧ 𝜂 ) ∧ 𝜓 ) → 𝜒 )
7		simpr	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜂 )
8	7	anim2i	⊢ ( ( ¬ 𝜓 ∧ ( 𝜑 ∧ 𝜂 ) ) → ( ¬ 𝜓 ∧ 𝜂 ) )
9	8	ancoms	⊢ ( ( ( 𝜑 ∧ 𝜂 ) ∧ ¬ 𝜓 ) → ( ¬ 𝜓 ∧ 𝜂 ) )
10	9 2	syl	⊢ ( ( ( 𝜑 ∧ 𝜂 ) ∧ ¬ 𝜓 ) → 𝜒 )
11	6 10	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜒 )