3ecase Show Code edit
# Inference for elimination by cases.
thm (3ecase () (3ecase.1 (-> (-. ph) th) 3ecase.2 (-> (-. ps) th) 3ecase.3 (-> (-. ch) th) 3ecase.4 (-> (/\/\ ph ps ch) th)) th 3ecase.4 3exp 3ecase.1 ch a1d ps a1d pm2.61i 3ecase.2 3ecase.3 pm2.61nii)
th
edit