exmid2

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

Step	Hyp	Ref	Expression
1		exmid2.1	$⊢ (ψ \land φ) \to χ$
2		exmid2.2	$⊢ (\neg ψ \land η) \to χ$
3		simpl	$⊢ (φ \land η) \to φ$
4	3	anim2i	$⊢ (ψ \land (φ \land η)) \to (ψ \land φ)$
5	4	ancoms	$⊢ ((φ \land η) \land ψ) \to (ψ \land φ)$
6	5 1	syl	$⊢ ((φ \land η) \land ψ) \to χ$
7		simpr	$⊢ (φ \land η) \to η$
8	7	anim2i	$⊢ (\neg ψ \land (φ \land η)) \to (\neg ψ \land η)$
9	8	ancoms	$⊢ ((φ \land η) \land \neg ψ) \to (\neg ψ \land η)$
10	9 2	syl	$⊢ ((φ \land η) \land \neg ψ) \to χ$
11	6 10	pm2.61dan	$⊢ (φ \land η) \to χ$

Metamath Proof Explorer