Theorem testable

Description: In classical logic all wffs are testable, that is, it is always true that ( -. ph \/ -. -. ph ) . This is not necessarily true in intuitionistic logic. In intuitionistic logic, if this statement is true for some ph , then ph istestable. The proof is trivial because it's simply a special case of the law of the excluded middle, which is true in classical logic but not necessarily true in intuitionisic logic. (Contributed by David A. Wheeler, 5-Dec-2018)

	Ref	Expression
Assertion	testable	$$⊢\left(\neg \phi \vee \neg \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		exmid	$$⊢\left(\neg \phi \vee \neg \neg \phi \right)$$