Theorem ifeq2da 4509

Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypothesis

Ref	Expression
ifeq2da.1	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifeq2da	⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Proof of Theorem ifeq2da

Step	Hyp	Ref	Expression
1		iftrue 4482	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2		iftrue 4482	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
3	1, 2	eqtr4d 2771	. . 3 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5		ifeq2da.1	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
6	5	ifeq2d 4497	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
7	4, 6	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-if 4477

This theorem is referenced by:  ifeq12da  4510  dfac12lem1  10046  ttukeylem3  10413  xmulcom  13172  xmulneg1  13175  subgmulg  19061  1marepvmarrepid  22510  pcopt2  24970  limcdif  25824  limcmpt  25831  limcres  25834  limccnp  25839  radcnv0  26372  leibpi  26899  efrlim  26926  efrlimOLD  26927  dchrvmasumiflem2  27460  padicabvf  27589  padicabvcxp  27590  itg2addnclem  37784  fourierdlem73  46339  fourierdlem76  46342  fourierdlem89  46355  fourierdlem91  46357