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

Metamath Proof Explorer

Theorem ifeqda

Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018)

Ref Expression
Hypotheses ifeqda.1 ⊢ φ ∧ ψ → A = C
ifeqda.2 ⊢ φ ∧ ¬ ψ → B = C
Assertion ifeqda ⊢ φ → if ψ A B = C

Proof

Step Hyp Ref Expression
1 ifeqda.1 ⊢ φ ∧ ψ → A = C
2 ifeqda.2 ⊢ φ ∧ ¬ ψ → B = C
3 iftrue ⊢ ψ → if ψ A B = A
4 3 adantl ⊢ φ ∧ ψ → if ψ A B = A
5 4 1 eqtrd ⊢ φ ∧ ψ → if ψ A B = C
6 iffalse ⊢ ¬ ψ → if ψ A B = B
7 6 adantl ⊢ φ ∧ ¬ ψ → if ψ A B = B
8 7 2 eqtrd ⊢ φ ∧ ¬ ψ → if ψ A B = C
9 5 8 pm2.61dan ⊢ φ → if ψ A B = C