Definition df-ifp 1047

Description: Definition of the conditional operator for propositions. The expression if-(𝜑, 𝜓, 𝜒) is read "if 𝜑 then 𝜓 else 𝜒". See dfifp2 1048, dfifp3 1049, dfifp4 1050, dfifp5 1051, dfifp6 1052 and dfifp7 1053 for alternate definitions.

This definition (in the form of dfifp2 1048) 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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	wif 1046	. 2 wff if-(𝜑, 𝜓, 𝜒)
5	1, 2	wa 386	. . 3 wff (𝜑 ∧ 𝜓)
6	1	wn 3	. . . 4 wff ¬ 𝜑
7	6, 3	wa 386	. . 3 wff (¬ 𝜑 ∧ 𝜒)
8	5, 7	wo 836	. 2 wff ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))
9	4, 8	wb 198	1 wff (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)))

This definition is referenced by:  dfifp2  1048  dfifp6  1052  ifpor  1055  casesifp  1060  ifpbi123d  1061  1fpid3  1063  wlk1walk  26986  upgriswlk  26988  bj-df-ifc  33144  ifpdfan  38772  ifpnot23  38785  upgrwlkupwlk  42767