Theory
SubAndCondContext
Parents
marker
Contents
Type operators
(none)
Constants
(none)
Definitions
(none)
Theorems
CASES_ELIM
Theorems
CASES_ELIM
⊢ ∀P p. P p ⇔ (p ⇒ P T) ∧ (¬p ⇒ P F)