Theorem ifeq2da 4512

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 4485	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2		iftrue 4485	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
3	1, 2	eqtr4d 2774	. . 3 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5		ifeq2da.1	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
6	5	ifeq2d 4500	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
7	4, 6	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-if 4480

This theorem is referenced by:  ifeq12da  4513  dfac12lem1  10054  ttukeylem3  10421  xmulcom  13181  xmulneg1  13184  subgmulg  19070  1marepvmarrepid  22519  pcopt2  24979  limcdif  25833  limcmpt  25840  limcres  25843  limccnp  25848  radcnv0  26381  leibpi  26908  efrlim  26935  efrlimOLD  26936  dchrvmasumiflem2  27469  padicabvf  27598  padicabvcxp  27599  itg2addnclem  37872  fourierdlem73  46423  fourierdlem76  46426  fourierdlem89  46439  fourierdlem91  46441