Metamath Proof Explorer

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- (φ, ψ, χ) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$

Proof

Step	Hyp	Ref	Expression
1		df-ifp	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$
2		cases2	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$
3	1 2	bitri	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$