Metamath Proof Explorer

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 ¬ φ ¬ ¬ φ


Step Hyp Ref Expression
1 exmid ¬ φ ¬ ¬ φ