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

Metamath Proof Explorer

Theorem ifsb

Description: Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013)

Ref Expression
Hypotheses ifsb.1 ⊢ if φ A B = A → C = D
ifsb.2 ⊢ if φ A B = B → C = E
Assertion ifsb ⊢ C = if φ D E

Proof

Step Hyp Ref Expression
1 ifsb.1 ⊢ if φ A B = A → C = D
2 ifsb.2 ⊢ if φ A B = B → C = E
3 iftrue ⊢ φ → if φ A B = A
4 3 1 syl ⊢ φ → C = D
5 iftrue ⊢ φ → if φ D E = D
6 4 5 eqtr4d ⊢ φ → C = if φ D E
7 iffalse ⊢ ¬ φ → if φ A B = B
8 7 2 syl ⊢ ¬ φ → C = E
9 iffalse ⊢ ¬ φ → if φ D E = E
10 8 9 eqtr4d ⊢ ¬ φ → C = if φ D E
11 6 10 pm2.61i ⊢ C = if φ D E