This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ifp	⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
2		cases2	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
3	1 2	bitri	⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )