Definition df-ifp 991

Description: Definition of the conditional operator for propositions. The expression if- ( ph , ps , ch ) is read "if ph then ps else ch". See dfifp2dc 994, dfifp3dc 995, dfifp4dc 996 and dfifp5dc 997 for alternate definitions.

This definition (in the form of dfifp2dc 994) 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 994 for compatibility with intuitionistic logic development: with this form, it is clear that if- ( ph , ps , ch ) implies decidability of ph (ifpdc 992), 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 990	. 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 720	. 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  992  ifp2  993  dfifp2dc  994  ifpor  1000  ifptru  1002  ifpfal  1003  ifpbi123d  1005  1fpid3  1007  wlk1walkdom  16583  upgriswlkdc  16584