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- ( 𝜑 , 𝜒 , 𝜃 ) )