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

Definition df-ifp 1033
 Description: Definition of the conditional operator for propositions. The value of if-(𝜑, 𝜓, 𝜒) is 𝜓 if 𝜑 is true and 𝜒 if 𝜑 false. See dfifp2 1034, dfifp3 1035, dfifp4 1036, dfifp5 1037, dfifp6 1038 and dfifp7 1039 for alternate definitions. This definition (in the form of dfifp2 1034) 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 wff with n+1 variables; single out one variable, say 𝜑; when one sets 𝜑 to True (resp. False), then what remains is a wff of n variables, so by the induction hypothesis it corresponds to a formula using only {if-, ⊤, ⊥}, say 𝜓 (resp. 𝜒); therefore, the formula if-(𝜑, 𝜓, 𝜒) represents the initial wff. Now, since { → , ¬ } and similar systems suffice to express 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 1032 . 2 wff if-(𝜑, 𝜓, 𝜒)
51, 2wa 383 . . 3 wff (𝜑𝜓)
61wn 3 . . . 4 wff ¬ 𝜑
76, 3wa 383 . . 3 wff 𝜑𝜒)
85, 7wo 382 . 2 wff ((𝜑𝜓) ∨ (¬ 𝜑𝜒))
94, 8wb 196 1 wff (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
 Colors of variables: wff setvar class This definition is referenced by:  dfifp2  1034  dfifp6  1038  ifpor  1041  casesifp  1046  ifpbi123d  1047  1fpid3  1049  wlk1walk  26591  upgriswlk  26593  bj-df-ifc  32690  ifpdfan  38127  ifpnot23  38140  upgrwlkupwlk  42046
 Copyright terms: Public domain W3C validator