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

Metamath Proof Explorer

Theorem eqif

Description: Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005)

Ref Expression
Assertion eqif ⊢ A = if φ B C ↔ φ ∧ A = B ∨ ¬ φ ∧ A = C

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ if φ B C = B → A = if φ B C ↔ A = B
2 eqeq2 ⊢ if φ B C = C → A = if φ B C ↔ A = C
3 1 2 elimif ⊢ A = if φ B C ↔ φ ∧ A = B ∨ ¬ φ ∧ A = C