Metamath Proof Explorer


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 φηχ