Theorem dfifp2

Description: Alternate definition of the conditional operator for propositions. The value of if- ( ph , ps , ch ) is "if ph then ps , and if not ph then ch ". This is the definition used in Section II.24 of Church p. 129 (Definition D12 page 132) (see comment of df-ifp ). (Contributed by BJ, 22-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		df-ifp	|- ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
2		cases2	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
3	1 2	bitri	|- ( if- ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )