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