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-φχθ