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

Metamath Proof Explorer

Theorem casesifp

Description: Version of cases expressed using if- . Case disjunction according to the value of ph . One can see this as a proof that the two hypotheses characterize the conditional operator for propositions. For the converses, see ifptru and ifpfal . (Contributed by BJ, 20-Sep-2019)

	Ref	Expression
Hypotheses	casesifp.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
	casesifp.2	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ 𝜃 ) )
Assertion	casesifp	⊢ ( 𝜓 ↔ if- ( 𝜑 , 𝜒 , 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		casesifp.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2		casesifp.2	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ 𝜃 ) )
3	1 2	cases	⊢ ( 𝜓 ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( ¬ 𝜑 ∧ 𝜃 ) ) )
4		df-ifp	⊢ ( if- ( 𝜑 , 𝜒 , 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( ¬ 𝜑 ∧ 𝜃 ) ) )
5	3 4	bitr4i	⊢ ( 𝜓 ↔ if- ( 𝜑 , 𝜒 , 𝜃 ) )