Definition df-ifp 984

Description: Definition of the conditional operator for propositions. The expression if-(𝜑, 𝜓, 𝜒) is read "if 𝜑 then 𝜓 else 𝜒". See dfifp2dc 987, dfifp3dc 988, dfifp4dc 989 and dfifp5dc 990 for alternate definitions.

This definition (in the form of dfifp2dc 987) 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).

This form was chosen as the definition rather than dfifp2dc 987 for compatibility with intuitionistic logic development: with this form, it is clear that if-(𝜑, 𝜓, 𝜒) implies decidability of 𝜑 (ifpdc 985), which is most often what is wanted.

(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 983	. 2 wff if-(𝜑, 𝜓, 𝜒)
5	1, 2	wa 104	. . 3 wff (𝜑 ∧ 𝜓)
6	1	wn 3	. . . 4 wff ¬ 𝜑
7	6, 3	wa 104	. . 3 wff (¬ 𝜑 ∧ 𝜒)
8	5, 7	wo 713	. 2 wff ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))
9	4, 8	wb 105	1 wff (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)))

This definition is referenced by:  ifpdc  985  ifp2  986  dfifp2dc  987  ifpor  993  ifptru  995  ifpfal  996  ifpbi123d  998  1fpid3  1000  wlk1walkdom  16080  upgriswlkdc  16081