 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ifp Structured version   Visualization version   GIF version

Definition df-ifp 1079
 Description: Definition of the conditional operator for propositions. The expression if-(𝜑, 𝜓, 𝜒) is read "if 𝜑 then 𝜓 else 𝜒". See dfifp2 1080, dfifp3 1081, dfifp4 1082, dfifp5 1083, dfifp6 1084 and dfifp7 1085 for alternate definitions. This definition (in the form of dfifp2 1080) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's [𝜓, 𝜑, 𝜒] corresponds to our if-(𝜑, 𝜓, 𝜒) (note the permutation of the first two variables). Church uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. The first result is that the system {if-, ⊤, ⊥} is complete: for the induction step, consider a formula of n+1 variables; single out one variable, say 𝜑; when one sets 𝜑 to True (resp. False), then what remains is a formula of n variables, so by the induction hypothesis it is equivalent to a formula using only the connectives if-, ⊤, ⊥, say 𝜓 (resp. 𝜒); therefore, the formula if-(𝜑, 𝜓, 𝜒) is equivalent to the initial formula of n+1 variables. Now, since { → , ¬ } and similar systems suffice to express the connectives if-, ⊤, ⊥, they are also complete. (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
df-ifp (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))

Detailed syntax breakdown of Definition df-ifp
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
41, 2, 3wif 1078 . 2 wff if-(𝜑, 𝜓, 𝜒)
51, 2wa 384 . . 3 wff (𝜑𝜓)
61wn 3 . . . 4 wff ¬ 𝜑
76, 3wa 384 . . 3 wff 𝜑𝜒)
85, 7wo 865 . 2 wff ((𝜑𝜓) ∨ (¬ 𝜑𝜒))
94, 8wb 197 1 wff (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
 Colors of variables: wff setvar class This definition is referenced by:  dfifp2  1080  dfifp6  1084  ifpor  1087  casesifp  1092  ifpbi123d  1093  1fpid3  1095  wlk1walk  26763  upgriswlk  26765  bj-df-ifc  32880  ifpdfan  38310  ifpnot23  38323  upgrwlkupwlk  42289
 Copyright terms: Public domain W3C validator