Theorem ifeq2da 4497

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1539  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-un 3897  df-if 4466

This theorem is referenced by:  ifeq12da  4498  dfac12lem1  9945  ttukeylem3  10313  xmulcom  13046  xmulneg1  13049  subgmulg  18814  1marepvmarrepid  21769  pcopt2  24231  limcdif  25085  limcmpt  25092  limcres  25095  limccnp  25100  radcnv0  25620  leibpi  26137  efrlim  26164  dchrvmasumiflem2  26695  padicabvf  26824  padicabvcxp  26825  itg2addnclem  35872  fourierdlem73  43769  fourierdlem76  43772  fourierdlem89  43785  fourierdlem91  43787