4cases Show Code edit
# Inference eliminating two antecedents from the four possible cases that
# result from their true/false combinations.
## Elimination by cases
thm (4cases () (4cases.1 (-> (/\ ph ps) ch) 4cases.2 (-> (/\ ph (-. ps)) ch) 4cases.3 (-> (/\ (-. ph) ps) ch) 4cases.4 (-> (/\ (-. ph) (-. ps)) ch)) ch 4cases.1 4cases.3 pm2.61ian 4cases.2 4cases.4 pm2.61ian pm2.61i)
ch
edit