Theorem ifeq2da 4563

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-if 4532

This theorem is referenced by:  ifeq12da  4564  dfac12lem1  10182  ttukeylem3  10549  xmulcom  13305  xmulneg1  13308  subgmulg  19171  1marepvmarrepid  22597  pcopt2  25070  limcdif  25926  limcmpt  25933  limcres  25936  limccnp  25941  radcnv0  26474  leibpi  27000  efrlim  27027  efrlimOLD  27028  dchrvmasumiflem2  27561  padicabvf  27690  padicabvcxp  27691  itg2addnclem  37658  fourierdlem73  46135  fourierdlem76  46138  fourierdlem89  46151  fourierdlem91  46153