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

Metamath Proof Explorer

Theorem ifval

Description: Another expression of the value of the if predicate, analogous to eqif . See also the more specialized iftrue and iffalse . (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion ifval ⊢ A = if φ B C ↔ φ → A = B ∧ ¬ φ → A = C

Proof

Step Hyp Ref Expression
1 eqif ⊢ A = if φ B C ↔ φ ∧ A = B ∨ ¬ φ ∧ A = C
2 cases2 ⊢ φ ∧ A = B ∨ ¬ φ ∧ A = C ↔ φ → A = B ∧ ¬ φ → A = C
3 1 2 bitri ⊢ A = if φ B C ↔ φ → A = B ∧ ¬ φ → A = C