Theorem ifeq2da 4515

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 4488	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2		iftrue 4488	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
3	1, 2	eqtr4d 2799	. . 3 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
4	3	adantl 487	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5		ifeq2da.1	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
6	5	ifeq2d 4503	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
7	4, 6	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-if 4483

This theorem is used by:  ifeq12da  4516  dfac12lem1  10215  ttukeylem3  10582  xmulcom  13389  xmulneg1  13392  subgmulg  19344  1marepvmarrepid  22883  pcopt2  25337  limcdif  26189  limcmpt  26196  limcres  26199  limccnp  26204  radcnv0  26736  leibpi  27263  efrlim  27290  dchrvmasumiflem2  27822  padicabvf  27951  padicabvcxp  27952  itg2addnclem  38569  fourierdlem73  47158  fourierdlem76  47161  fourierdlem89  47174  fourierdlem91  47176