Definition df-ifp 986

Description: Definition of the conditional operator for propositions. The expression if- ( ph , ps , ch ) is read "if ph then ps else ch". 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 [ ps , ph , ch ] corresponds to our if- ( ph , ps , ch ) (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- ( ph , ps , ch ) implies decidability of ph (ifpdc 987), which is most often what is wanted.

(Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-ifp	|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )

Detailed syntax breakdown of Definition df-ifp

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	wif 985	. 2 wff if- ( ph , ps , ch )
5	1, 2	wa 104	. . 3 wff ( ph /\ ps )
6	1	wn 3	. . . 4 wff -. ph
7	6, 3	wa 104	. . 3 wff ( -. ph /\ ch )
8	5, 7	wo 715	. 2 wff ( ( ph /\ ps ) \/ ( -. ph /\ ch ) )
9	4, 8	wb 105	1 wff (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )

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