Definition df-ifp 986

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

This definition (in the form of dfifp2dc 989) 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 989 for compatibility with intuitionistic logic development: with this form, it is clear that if-(𝜑, 𝜓, 𝜒) implies decidability of 𝜑 (ifpdc 987), 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 985	. 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 715	. 2 wff ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))
9	4, 8	wb 105	1 wff (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)))

This definition is referenced by:  ifpdc  987  ifp2  988  dfifp2dc  989  ifpor  995  ifptru  997  ifpfal  998  ifpbi123d  1000  1fpid3  1002  wlk1walkdom  16216  upgriswlkdc  16217