<gh_stars>0
{
  "citations" : [ {
    "textCitation" : "[See casesifp on Metamath](http://us.metamath.org/mpegif/casesifp.html)"
  } ],
  "names" : [ "casesifp" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_wph", "#T_wi", "#T_wps", "#T_wb", "#T_wch", "#T_wn", "#T_wph", "#T_wi", "#T_wps", "#T_wb", "#T_wth", "#T_wps", "#T_wb", "#T_wif--1", "#T_wph", "#T_wif--2", "#T_wch", "#T_wif--3", "#T_wth" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " Version of ~ cases expressed using ` if- ` .  Case disjunction according to the value of ` ph ` .  One can see this as a proof that the two hypotheses characterize the conditional operator for propositions. (Contributed by BJ, 20-Sep-2019.) ",
  "statement" : "casesifp.1 $e |- ( ph -> ( ps <-> ch ) ) $.\ncasesifp.2 $e |- ( -. ph -> ( ps <-> th ) ) $.\ncasesifp $p |- ( ps <-> if- ( ph , ch , th ) ) $."
}