Theorem exmid2

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

	Ref	Expression
Hypotheses	exmid2.1	|- ( ( ps /\ ph ) -> ch )
	exmid2.2	|- ( ( -. ps /\ et ) -> ch )
Assertion	exmid2	|- ( ( ph /\ et ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		exmid2.1	|- ( ( ps /\ ph ) -> ch )
2		exmid2.2	|- ( ( -. ps /\ et ) -> ch )
3		simpl	|- ( ( ph /\ et ) -> ph )
4	3	anim2i	|- ( ( ps /\ ( ph /\ et ) ) -> ( ps /\ ph ) )
5	4	ancoms	|- ( ( ( ph /\ et ) /\ ps ) -> ( ps /\ ph ) )
6	5 1	syl	|- ( ( ( ph /\ et ) /\ ps ) -> ch )
7		simpr	|- ( ( ph /\ et ) -> et )
8	7	anim2i	|- ( ( -. ps /\ ( ph /\ et ) ) -> ( -. ps /\ et ) )
9	8	ancoms	|- ( ( ( ph /\ et ) /\ -. ps ) -> ( -. ps /\ et ) )
10	9 2	syl	|- ( ( ( ph /\ et ) /\ -. ps ) -> ch )
11	6 10	pm2.61dan	|- ( ( ph /\ et ) -> ch )